Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 45428f88 by sheaf at 2026-03-26T03:51:31-04:00 Avoid infinite loop in deep subsumption This commit ensures we only unify after we recur in the deep subsumption code in the FunTy vs non-FunTy case of GHC.Tc.Utils.Unify.tc_sub_type_deep, to avoid falling into an infinite loop. See the new Wrinkle [Avoiding a loop in tc_sub_type_deep] in Note [FunTy vs non-FunTy case in tc_sub_type_deep] in GHC.Tc.Utils.Unify. Fixes #26823 Co-authored-by: simonpj - - - - - 5 changed files: - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/typecheck/should_compile/T26225.hs - + testsuite/tests/typecheck/should_fail/T26823.hs - + testsuite/tests/typecheck/should_fail/T26823.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -1948,6 +1948,41 @@ the LHS vs the new RHS. And vice-versa (if it's the RHS that is a FunTy). See T11305 and T26225 for examples of when this is important. +Wrinkle [Avoiding a loop in tc_sub_type_deep] + + In #26823, we had: + + alpha <= a -> alpha + + If we simply unified the two types, the occurs-check would trigger. + In deep subsumption however, we need to be careful, as we might do the + following: + + A1. Create fresh metavariables beta, gamma + A2. Unify alpha ~ beta -> gamma + A3. Decompose "beta -> gamma <= a -> (beta -> gamma)", obtaining + a <= beta and gamma <= beta -> gamma + A4. Recur with gamma <= beta -> gamma + + If we do this, we enter an infinite loop and GHC hangs at compile time. + To avoid this, we must first recur, before unifying. So the above becomes: + + B1 (like A1). Create fresh metavariables beta, gamma + B2 (like A3). Decompose "beta -> gamma <= a -> alpha", obtaining + a <= beta and gamma <= alpha + B3. Solve these two sub-problems by unification + a ~ beta, gamma ~ alpha + B4 (like A2). Then, and only then, unify alpha ~ beta->gamma + + With this approach, GHC will be left with the following unifications: + + - alpha ~ (beta -> gamma) + - a ~ beta + - gamma ~ alpha + + GHC will fail to solve this unification problem due to an occurs check + failure, thus rejecting the program with a type error (as desired). + Note [Deep subsumption and required foralls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A required forall, (forall a -> ty) behaves like a "rho-type", one with no @@ -2117,8 +2152,9 @@ tc_sub_type_deep fun_pos@(tc_fun, pos) ds_depth unify inst_orig ctxt ty_actual t ; exp_arg <- newOpenFlexiTyVarTy -- NB: no FRR check needed; we might not need to eta-expand ; exp_res <- newOpenFlexiTyVarTy ; let exp_funTy = FunTy { ft_af = af1, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res } - ; unify_wrap <- just_unify exp_funTy ty_e + -- Recur before unifying; see Wrinkle [Avoiding a loop in tc_sub_type_deep] ; fun_wrap <- go_fun af1 act_mult act_arg act_res af1 exp_mult exp_arg exp_res + ; unify_wrap <- just_unify exp_funTy ty_e ; return $ unify_wrap <.> fun_wrap -- unify_wrap :: exp_funTy ~~> ty_e -- fun_wrap :: ty_a ~~> exp_funTy @@ -2129,8 +2165,9 @@ tc_sub_type_deep fun_pos@(tc_fun, pos) ds_depth unify inst_orig ctxt ty_actual t ; act_arg <- newOpenFlexiTyVarTy -- NB: no FRR check needed; we might not need to eta-expand ; act_res <- newOpenFlexiTyVarTy ; let act_funTy = FunTy { ft_af = af2, ft_mult = act_mult, ft_arg = act_arg, ft_res = act_res } - ; unify_wrap <- just_unify ty_a act_funTy + -- Recur before unifying; see Wrinkle [Avoiding a loop in tc_sub_type_deep] ; fun_wrap <- go_fun af2 act_mult act_arg act_res af2 exp_mult exp_arg exp_res + ; unify_wrap <- just_unify ty_a act_funTy ; return $ fun_wrap <.> unify_wrap -- unify_wrap :: ty_a ~~> act_funTy -- fun_wrap :: act_funTy ~~> ty_e ===================================== testsuite/tests/typecheck/should_compile/T26225.hs ===================================== @@ -26,7 +26,7 @@ ex0 = in g f -- ((∀ a. a->a) -> Int) -> Bool ⊑ α[tau] --- Rejected by GHC up to and including 9.14. +-- Rejected by GHC up to and including 9.12. ex1' :: () ex1' = let @@ -38,7 +38,7 @@ ex1' = -- Couldn't match expected type ‘α’ with actual type ‘((∀ a. a -> a) -> Int) -> Bool’ -- ((∀ a. a->a) -> Int) -> Bool ⊑ β[tau] Bool --- Rejected by GHC up to and including 9.14. +-- Rejected by GHC up to and including 9.12. ex2' :: () ex2' = let @@ -50,7 +50,7 @@ ex2' = -- Couldn't match expected type ‘β’ with actual type ‘(->) ((∀ a. a -> a) -> Int)’ -- ex3 :: β[tau] Bool ⊑ (∀ a. a->a) -> Bool --- Rejected by GHC up to and including 9.14. +-- Rejected by GHC up to and including 9.12. ex3 :: () ex3 = let @@ -62,7 +62,7 @@ ex3 = -- Couldn't match expected type ‘β’ with actual type ‘(->) (∀ a. a -> a)’ -- ex3' :: F Int Bool ⊑ (∀ a. a->a) -> Bool, where F Int = (->) (Int -> Int) --- Rejected by GHC up to and including 9.14. +-- Rejected by GHC up to and including 9.12. ex3' :: () ex3' = let ===================================== testsuite/tests/typecheck/should_fail/T26823.hs ===================================== @@ -0,0 +1,15 @@ +{-# LANGUAGE DeepSubsumption #-} + +module T26823 where + +allocArray :: Int -> IO () +allocArray n = do + let + !off = 18 + !size = 8 + !vecAli = size + + !rem = off `rem` vecAli + !start = if rem == 0 then off else off + ( vecAli - rem ) + + return () ===================================== testsuite/tests/typecheck/should_fail/T26823.stderr ===================================== @@ -0,0 +1,32 @@ +T26823.hs:12:14: error: [GHC-25897] + • Couldn't match expected type ‘a0 -> a0 -> t’ with actual type ‘t’ + ‘t’ is a rigid type variable bound by + the inferred type of rem :: a0 -> a0 -> t + at T26823.hs:12:5-29 + • In the expression: off `rem` vecAli + In an equation for ‘rem’: !rem = off `rem` vecAli + In a stmt of a 'do' block: + let !off = 18 + !size = 8 + !vecAli = size + !rem = off `rem` vecAli + !start = if rem == 0 then off else off + (vecAli - rem) + • Relevant bindings include + rem :: a0 -> a0 -> t (bound at T26823.hs:12:6) + off :: a0 (bound at T26823.hs:8:6) + vecAli :: a0 (bound at T26823.hs:10:6) + size :: a0 (bound at T26823.hs:9:6) + +T26823.hs:13:57: error: [GHC-27958] + • Couldn't match expected type ‘a0’ + with actual type ‘a0 -> a0 -> t0’ + • In the second argument of ‘(-)’, namely ‘rem’ + In the second argument of ‘(+)’, namely ‘(vecAli - rem)’ + In the expression: off + (vecAli - rem) + • Relevant bindings include + start :: a0 (bound at T26823.hs:13:6) + rem :: forall {t}. a0 -> a0 -> t (bound at T26823.hs:12:6) + off :: a0 (bound at T26823.hs:8:6) + vecAli :: a0 (bound at T26823.hs:10:6) + size :: a0 (bound at T26823.hs:9:6) + ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -755,5 +755,6 @@ test('T23162a', normal, compile_fail, ['']) test('T23162b', normal, compile_fail, ['']) test('T23162c', normal, compile, ['']) test('T23162d', normal, compile, ['']) +test('T26823', normal, compile_fail, ['']) test('T26861', normal, compile_fail, ['']) test('T26862', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/45428f88f62896650156dc8222299744... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/45428f88f62896650156dc8222299744... You're receiving this email because of your account on gitlab.haskell.org.