Fix #2073.

CHANGELOG.md

@@ -23,6 +23,10 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
 * Compiler crash due to the type checker forgetting to respect the
   explicitly ascribed non-consuming diet of loop parameters (#2067).
 
+* Size inference did incomplete level/scope checking, which could
+  result in circular sizes, which usually manifested as the type
+  checker going into an infinite loop (#2073).
+
 ## [0.25.11]
 
 ### Added

src/Language/Futhark/TypeChecker/Terms.hs

@@ -614,9 +614,9 @@ checkExp (AppExp (LetPat sizes pat e body loc) _) = do
   -- Not technically an ascription, but we want the pattern to have
   -- exactly the type of 'e'.
   t <- expType e'
-  incLevel . bindingSizes sizes $ \sizes' ->
-    bindingPat sizes' pat t $ \pat' -> do
-      body' <- checkExp body
+  bindingSizes sizes $ \sizes' ->
+    incLevel . bindingPat sizes' pat t $ \pat' -> do
+      body' <- incLevel $ checkExp body
       body_t <- expTypeFully body'
 
       -- If the bound expression is of type i64, then we replace the

src/Language/Futhark/TypeChecker/Terms/Pat.hs

@@ -346,4 +346,4 @@ bindingParams tps orig_ps m = do
             binding (patIdents $ fmap toStruct p') $ incLevel $ descend (p' : ps') ps
         descend ps' [] = m tps' $ reverse ps'
 
-    descend [] orig_ps
+    incLevel $ descend [] orig_ps

src/Language/Futhark/TypeChecker/Unify.hs

@@ -817,9 +817,18 @@ linkVarToDim usage bcs vn lvl e = do
 
   modifyConstraints $ M.insert vn (lvl, Size (Just e) usage)
   where
+    checkVar _ dim'
+      | vn == dim' = do
+          notes <- dimNotes usage e
+          unifyError usage notes bcs $
+            "Occurs check: cannot instantiate"
+              <+> dquotes (prettyName vn)
+              <+> "with"
+              <+> dquotes (pretty e)
+              <+> "."
     checkVar constraints dim'
       | Just (dim_lvl, c) <- dim' `M.lookup` constraints,
-        dim_lvl > lvl =
+        dim_lvl >= lvl =
           case c of
             ParamSize {} -> do
               notes <- dimNotes usage e
@@ -831,17 +840,10 @@ linkVarToDim usage bcs vn lvl e = do
                   <+> "(scope violation)."
                   </> "This is because"
                   <+> dquotes (pretty $ qualName dim')
-                  <+> "is rigidly bound in a deeper scope."
+                  <+> "is not in scope when"
+                  <+> dquotes (prettyName vn)
+                  <+> "is introduced."
             _ -> modifyConstraints $ M.insert dim' (lvl, c)
-    checkVar _ dim'
-      | vn == dim' = do
-          notes <- dimNotes usage e
-          unifyError usage notes bcs $
-            "Occurs check: cannot instantiate"
-              <+> dquotes (prettyName vn)
-              <+> "with"
-              <+> dquotes (pretty e)
-              <+> "."
     checkVar _ _ = pure ()
 
 -- | Assert that this type must be one of the given primitive types.
@@ -1221,7 +1223,7 @@ instance MonadUnify UnifyM where
           M.insert dim (0, Size Nothing usage)
     pure dim
 
-  curLevel = pure 0
+  curLevel = pure 1
 
   unifyError loc notes bcs doc =
     throwError $ TypeError (locOf loc) notes $ doc <> pretty bcs
@@ -1243,8 +1245,8 @@ runUnifyM rigid_tparams nonrigid_tparams (UnifyM m) =
     constraints =
       M.fromList $
         map nonrigid nonrigid_tparams <> map rigid rigid_tparams
-    nonrigid (TypeParamDim p loc) = (p, (0, Size Nothing $ Usage Nothing loc))
-    nonrigid (TypeParamType l p loc) = (p, (0, NoConstraint l $ Usage Nothing loc))
+    nonrigid (TypeParamDim p loc) = (p, (1, Size Nothing $ Usage Nothing loc))
+    nonrigid (TypeParamType l p loc) = (p, (1, NoConstraint l $ Usage Nothing loc))
     rigid (TypeParamDim p loc) = (p, (0, ParamSize loc))
     rigid (TypeParamType l p loc) = (p, (0, ParamType l loc))
 

tests/issue2073.fut

@@ -0,0 +1,11 @@
+-- ==
+-- error: "value" is not in scope
+
+def f [n] (dmax: i64) (depth: [n]i64) (value: [n]i32) (parent: [n]i64) : []i32 =
+  loop value for d in dmax..dmax-1...1 do
+    reduce_by_index
+    (copy value)
+    (+)
+    0i32
+    (map (\i -> if depth[i] == d then parent[i] else -1) (iota (length value)))
+    value

tests/types/ext4.fut

@@ -2,4 +2,4 @@
 -- input { [true] [2] }
 -- output { 1i64 }
 
-def main [n] (xs: ?[n].[n]bool) (ys: [n]i32) = length (zip xs ys)
+def main [n] (xs: ?[m].[m]bool) (ys: [n]i32) = length (zip xs ys)