GitLab

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 <simon.peytonjones@gmail.com>

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

 +{-# 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

 +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, [''])