Increment level for each function parameter.

This addresses a *really* obscure bug related to inferring parameters
of the form

  (A: [length A]t)

which can cause type normalisation to go into an infinite loop in some
cases (because of the type annotation on the 'A' variable).

src/Language/Futhark/TypeChecker/Terms.hs

@@ -1695,7 +1695,7 @@ letGeneralise defname defloc tparams params restype =
     let keep_type_vars = overloadedTypeVars now_substs
 
     cur_lvl <- curLevel
-    let candidate k (lvl, _) = (k `S.notMember` keep_type_vars) && lvl >= cur_lvl
+    let candidate k (lvl, _) = (k `S.notMember` keep_type_vars) && lvl >= (cur_lvl - length params)
         new_substs = M.filterWithKey candidate now_substs
 
     (tparams', RetType ret_dims restype') <-

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

@@ -343,7 +343,7 @@ bindingParams tps orig_ps m = do
   checkTypeParams tps $ \tps' -> bindingTypeParams tps' $ do
     let descend ps' (p : ps) =
           checkPat [] p NoneInferred $ \p' ->
-            binding (patIdents $ fmap toStruct p') $ descend (p' : ps') ps
+            binding (patIdents $ fmap toStruct p') $ incLevel $ descend (p' : ps') ps
         descend ps' [] = m tps' $ reverse ps'
 
     descend [] orig_ps

tests/shapes/funshape2.fut

@@ -1,4 +1,4 @@
 -- ==
--- error: Causality check
+-- error: scope violation
 
 def main xs = (\f' -> f' (filter (>0) xs)) (\_ -> 0)

tests/shapes/size-inference4.fut

@@ -2,6 +2,6 @@
 -- parameter.  Written in a convoluted way to ensure this is checked
 -- even for lambdas that are never let-generalised.
 -- ==
--- error: refers to size "n"
+-- error: scope violation
 
 def f : i32 = const 2 ((\xs n -> (zip xs (iota n) : [](i64, i64))))

tests/shapes/size-inference5.fut

@@ -1,5 +1,5 @@
 -- Like size-inference4.fut, but with a let-binding.
 -- ==
--- error: refers to size "n"
+-- error: scope violation
 
 def f xs n = zip xs (iota n)