Fix #2193.

This turns out to be an overall simplification and loosening of
language restrictions.

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]

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

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

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

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)

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]