From bf57ad951f1eda6804d58dc6bc9394b0966927f8 Mon Sep 17 00:00:00 2001 From: Troels Henriksen Date: Wed, 6 Dec 2023 00:12:08 +0100 Subject: [PATCH] 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 | 2 +- src/Language/Futhark/TypeChecker/Terms/Pat.hs | 2 +- tests/shapes/funshape2.fut | 2 +- tests/shapes/size-inference4.fut | 2 +- tests/shapes/size-inference5.fut | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Language/Futhark/TypeChecker/Terms.hs b/src/Language/Futhark/TypeChecker/Terms.hs index 37249ee617..14eeb58b06 100644 --- a/src/Language/Futhark/TypeChecker/Terms.hs +++ b/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') <- diff --git a/src/Language/Futhark/TypeChecker/Terms/Pat.hs b/src/Language/Futhark/TypeChecker/Terms/Pat.hs index 30eb41853c..63c65545b0 100644 --- a/src/Language/Futhark/TypeChecker/Terms/Pat.hs +++ b/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 diff --git a/tests/shapes/funshape2.fut b/tests/shapes/funshape2.fut index cef48c3e56..4fb6523f0f 100644 --- a/tests/shapes/funshape2.fut +++ b/tests/shapes/funshape2.fut @@ -1,4 +1,4 @@ -- == --- error: Causality check +-- error: scope violation def main xs = (\f' -> f' (filter (>0) xs)) (\_ -> 0) diff --git a/tests/shapes/size-inference4.fut b/tests/shapes/size-inference4.fut index 1d7cd3d0cc..e53f5b158c 100644 --- a/tests/shapes/size-inference4.fut +++ b/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)))) diff --git a/tests/shapes/size-inference5.fut b/tests/shapes/size-inference5.fut index 2533da45c5..dbdae8f9ee 100644 --- a/tests/shapes/size-inference5.fut +++ b/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)