GitLab

Simon Peyton Jones pushed to branch wip/26543 at Glasgow Haskell Compiler / GHC

Commits:

2d55348a

by Simon Peyton Jones at 2025-11-03T23:40:29+00:00

Improve simpleUnifyCheck and coercion holes

Fixes #26543.

Rahter rejecting holes, look in the kind of the hole

4 changed files:

compiler/GHC/Tc/Gen/App.hs
compiler/GHC/Tc/Utils/Unify.hs
+ testsuite/tests/impredicative/T26543.hs
testsuite/tests/impredicative/all.T

Changes:

compiler/GHC/Tc/Gen/App.hs

@@ -2057,6 +2057,7 @@ qlUnify ty1 ty2
                -- Here we are in the TcM monad, which does not track enclosing
                -- Given equalities; so for quick-look unification we conservatively
                -- treat /any/ level outside this one as untouchable. Hence cur_lvl.
 +              -- See (UQL5) in Note [QuickLook unification]
             ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of
                SUC_CanUnify ->
                  do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
@@ -2129,6 +2130,17 @@ That is the entire point of qlUnify!   Wrinkles:
    It's just not worth the trouble, we think (for now at least).
 +(UQL5) We call `simpleUnifyCheck` for the occurs-check etc; see (UQL1). Usually it's fine
 +  for `simpleUnifyCheck` to bale out saying `SUC_NotSure`, because usually we'll just generate
 +  an equality we solve later. But in QuickLook, baling out may mean we don't find a good
 +  type for an instantiation variable, which in turn may make the program fail to typecheck.
 +  So `simpleUnifyCheck` is more than just an erfficiency thing.
 +  Example (#26543): we get qlUnify( (Eq (alpha |> {co}) => beta) -> Int
 +                                  , kappa1                       -> Int )
 +  where `{co}` is a coercion hole. We want to unify
 +    kappa1 := Eq (alpha |> {co}) => beta
 +  Failing to do so rejects the program.  To allow this, we just check the /kind/ of the
 +  coercion hole {co}; see
  Sadly discarded design alternative
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

compiler/GHC/Tc/Utils/Unify.hs

@@ -3194,6 +3194,8 @@ simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUn
  -- * Rejects type families unless fam_ok=True
  -- * Does a level-check for type variables, to avoid skolem escape
  --
 +-- See also (UQL5) in Note [QuickLook unification]
 +--
  -- This function is pretty heavily used, so it's optimised not to allocate
  simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
    | not $ touchabilityTest given_eq_lvl lhs_tv
@@ -3254,9 +3256,11 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
  mkOccFolders :: Name -> (TcType -> Bool, TcCoercion -> Bool)
 --- These functions return True
 ---   * if lhs_tv occurs (incl deeply, in the kind of variable)
 ---   * if there is a coercion hole
 +-- These functions are used when doing an occurs check.
 +-- They return True if lhs_tv occurs in the type, or coercion resp,
 +-- including deeply,
 +--    - in the kind of type variable
 +--    - in the kind of a coercion hole
  -- No expansion of type synonyms
  mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co)
    where
@@ -3270,7 +3274,14 @@ mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co)
                    `mappend` check_ty (varType v)
      do_bndr is tcv _faf = extendVarSet is tcv
 -    do_hole _is _hole = DM.Any True  -- Reject coercion holes
++
 +    do_hole _is hole = check_ty (varType (coHoleCoVar hole))
 +       -- For coercion holes, look in the kind of the hole
 +       -- I worry that the coercion hole could be filled with a coercion that
 +       -- mentions `lhs_tv` in the coercion, but not in the /kind/ of that
 +       -- coercion.  But that seems remote; and it is the /same/ choice that is
 +       -- made in `GHC.Tc.Utils.Unify.checkCo`.
 +       -- See (UQL5) in Note [QuickLook unification]
  {- *********************************************************************
  *                                                                      *

testsuite/tests/impredicative/T26543.hs

 +{-# LANGUAGE GHC2024, TypeAbstractions, AllowAmbiguousTypes, TypeFamilies #-}
 +module T26543 where
++
 +import Data.Kind (Type)
++
 +withObProd :: forall a r. ((Eq a) => r) -> r
 +withObProd = withObProd
++
 +type Ap :: k -> Type
 +data Ap a where
 +  Ap :: forall {k} (a :: k). Ap a
++
 +type family Ap2 :: Type -> Type
 +type instance Ap2 = Ap
++
 +f :: forall (a :: Type). Ap2 a -> Bool
 +f (Ap @x') = withObProd @x' $ True
++
++
 +-- ($) :: (p->q) -> p -> q
 +-- QL sees that: p = Eq a => Bool
 +--               q = Bool

testsuite/tests/impredicative/all.T

@@ -22,3 +22,4 @@ test('T17332', normal, compile_fail, [''])
  test('expr-sig', normal, compile, [''])
  test('Dict', normal, compile, [''])
  test('T24676', normal, compile, [''])
 +test('T26543', normal, compile, [''])