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 ===================================== @@ -0,0 +1,22 @@ +{-# 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, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2d55348a4607da243f90049201338f7c... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2d55348a4607da243f90049201338f7c... You're receiving this email because of your account on gitlab.haskell.org.