From 10fcc490c60d3546350ecddb7fdb63310065100d Mon Sep 17 00:00:00 2001 From: Troels Henriksen Date: Tue, 19 Nov 2024 23:12:05 +0100 Subject: [PATCH] Fix #2193. This turns out to be an overall simplification and loosening of language restrictions. --- CHANGELOG.md | 3 ++ docs/error-index.rst | 63 ----------------------- src/Language/Futhark/TypeChecker/Unify.hs | 27 ++++++---- tests/issue2193.fut | 4 ++ tests/types/ext6.fut | 5 +- tests/types/ext7.fut | 2 +- 6 files changed, 27 insertions(+), 77 deletions(-) create mode 100644 tests/issue2193.fut diff --git a/CHANGELOG.md b/CHANGELOG.md index d2fa5aa9ec..45e2138978 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,9 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0. ### Fixed +* Sizes that go out of scope due to use of higher order functions will + now work in more cases by adding existentials. (#2193) + ### Changed ## [0.25.24] diff --git a/docs/error-index.rst b/docs/error-index.rst index 9901c360dc..70c222fd3e 100644 --- a/docs/error-index.rst +++ b/docs/error-index.rst @@ -566,69 +566,6 @@ Such an abbreviation is actually shorthand for which is erroneous, but with workarounds, as explained in :ref:`unused-existential`. -.. _unify-param-existential: - -"Parameter *x* used as size would go out of scope." -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -This error tends to happen when higher-order functions are used in a -way that causes a size requirement to become impossible to express. -Real programs that encounter this issue tend to be complicated, but to -illustrate the problem, consider the following contrived function: - -.. code-block:: futhark - - def f (n: i64) (m: i64) (b: [n][m]bool) = b[0,0] - -We have the following type: - -.. code-block:: futhark - - val f : (n: i64) -> (m: i64) -> (b: [n][m]bool) -> bool - -Now suppose we say: - -.. code-block:: futhark - - def g = uncurry f - -What should be the type of ``g``? Intuitively, something like this: - -.. code-block:: futhark - - val g : (n: i64, m: i64) -> (b: [n][m]bool) -> bool - -But this is *not* expressible in the Futhark type system - and even if -it were, it would not be easy to infer this in general, as it depends -on exactly what ``uncurry`` does, which the type checker does not -know. - -As a workaround, we can use explicit type annotation and size -coercions to give ``g`` an acceptable type: - -.. code-block:: futhark - - def g [a][b] (n,m) (b: [a][b]bool) = f n m (b :> [n][m]bool) - -Another workaround, which is often the right one in cases not as -contrived as above, is to modify ``f`` itself to produce a *witness* -of the constraint, in the form of an array of shape ``[n][m]``: - -.. code-block:: futhark - - def f (n: i64) (m: i64) : ([n][m](), [n][m]bool -> bool) = - (replicate n (replicate m ()), \b -> b[0,0]) - -Then ``uncurry f`` works just fine and has the following type: - -.. code-block:: futhark - - (i64, i64) -> ?[n][m].([n][m](), [n][m]bool -> bool) - -Programming with such *explicit size witnesses* is a fairly advanced -technique, but often necessary when writing advanced size-dependent -code. - .. _unify-consuming-param: "Parameter types *x* and *y* are incompatible regarding consuming their arguments diff --git a/src/Language/Futhark/TypeChecker/Unify.hs b/src/Language/Futhark/TypeChecker/Unify.hs index d013d685be..5638acdc9e 100644 --- a/src/Language/Futhark/TypeChecker/Unify.hs +++ b/src/Language/Futhark/TypeChecker/Unify.hs @@ -706,20 +706,24 @@ linkVarToType onDims usage bound bcs vn lvl tp_unnorm = do occursCheck usage bcs vn tp scopeCheck usage bcs vn lvl tp - constraints <- getConstraints let link = do let (witnessed, not_witnessed) = determineSizeWitnesses tp used v = v `S.member` witnessed || v `S.member` not_witnessed - ext = filter used bound - case filter (`notElem` witnessed) ext of - [] -> - modifyConstraints $ - M.insert vn (lvl, Constraint (RetType ext tp) usage) - problems -> - unifyError usage mempty bcs . withIndexLink "unify-param-existential" $ - "Parameter(s) " - <> commasep (map (dquotes . prettyName) problems) - <> " used as size(s) would go out of scope." + (ext_witnessed, ext_not_witnessed) = + L.partition (`elem` witnessed) $ filter used bound + + -- Any size that uses an ext_not_witnessed variable must + -- be replaced with a fresh existential. + problematic e = + L.find (`elem` ext_not_witnessed) $ + S.toList $ + fvVars $ + freeInExp e + + (tp', ext_new) <- sizeFree (srclocOf usage) problematic tp + + modifyConstraints $ + M.insert vn (lvl, Constraint (RetType (ext_new <> ext_witnessed) tp') usage) let unliftedBcs unlifted_usage = breadCrumb @@ -731,6 +735,7 @@ linkVarToType onDims usage bound bcs vn lvl tp_unnorm = do ) bcs + constraints <- getConstraints case snd <$> M.lookup vn constraints of Just (NoConstraint Unlifted unlift_usage) -> do link diff --git a/tests/issue2193.fut b/tests/issue2193.fut new file mode 100644 index 0000000000..d5bc483e4f --- /dev/null +++ b/tests/issue2193.fut @@ -0,0 +1,4 @@ +def takefrom 't (xs: []t) (i: i64) : [i+1]t = take (i+1) xs + +entry main n (xs: []i32) = + n |> takefrom xs diff --git a/tests/types/ext6.fut b/tests/types/ext6.fut index 3b1ff2fd28..fd9258fe10 100644 --- a/tests/types/ext6.fut +++ b/tests/types/ext6.fut @@ -1,8 +1,9 @@ -- == --- error: used as size +-- input { 1i64 2i64 } +-- output { [[true, true]] } def f (n: i64) (m: i64) (b: bool) = replicate n (replicate m b) def g = uncurry f -def main x = map id (g x true) +def main a b = map id (g (a,b) true) diff --git a/tests/types/ext7.fut b/tests/types/ext7.fut index 018d06991c..95d501e844 100644 --- a/tests/types/ext7.fut +++ b/tests/types/ext7.fut @@ -1,5 +1,5 @@ -- == --- error: used as size +-- error: Existential size would appear def f (n: i64) (m: i64) (b: [n][m]bool) = b[0,0]