Simon Peyton Jones pushed to branch wip/T26543b at Glasgow Haskell Compiler / GHC Commits: defc3eae by Simon Peyton Jones at 2026-08-23T00:01:34+01:00 Line up simpleUnifyCheck and check_ty_eq_rhs Even after #26543 was allegedly fixed, the original repo case in the Description continued to fail. The reason was that the QuickLook unifier, `qlUnify`, used `simpleUnifyCheck` for checking unification invariants; and `simpleUnifyCheck` conservatively rejected any RHS with a coercion hole in it. The upshot was that QuickLook was not as clever as it should be, wrongly failing to do an impredicative instantiation. Interestingly `check_ty_eq_rhs`, which does the same job, only during constraint solving, was more liberal: it just looked at the free vars of the coercion, and allowed coercion holes. This MR lines them up, adding some careful notes. See Note [simpleUnifyCheck] esp (SUC1) Note [Unification preconditions] esp (COERCIONS) Things are better than before, but I am still uncomfortable about the possibilty that a hole might be filled with a coercion that mentions the LHS type variable; for now I have left this discomfort documented in (SUC1). - - - - - 6 changed files: - + changelog.d/T26543 - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/typecheck/should_compile/T26543_orig.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== changelog.d/T26543 ===================================== @@ -0,0 +1,7 @@ +section: compiler +synopsis: Fix a bug in ImpredicativeTypes +description: + The QuickLook algorithm (which implements `ImpredicativeTypes`) was defeated if there + was a kind coercion in the types being unified. That bug is now fixed. +mrs: !16566 +issues: #26543 ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -850,15 +850,15 @@ invisibleVarsOfTypes = foldr (unionVarSet . invisibleVarsOfType) emptyVarSet {-# INLINE afvFolder #-} -- so that specialization to (const True) works afvFolder :: (TyCoVar -> Bool) -> TyCoFolder (FV TyCoVarSet DM.Any) -- 'afvFolder' is short for "any-free-var folder", good for checking --- if any free var of a type satisfies a predicate `check_fv` +-- if any shallow free var of a type satisfies a predicate `check_fv` afvFolder check_fv = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms] , tcf_tyvar = do_tcv, tcf_covar = do_tcv , tcf_hole = do_hole , tcf_tycobinder = addBndrFV } where - do_tcv tv = MkFV $ \ bvs -> - Any (not (tv `elemVarSet` bvs) && check_fv tv) - do_hole _ = mempty -- I'm unsure; probably never happens + do_tcv tv = MkFV $ \ bvs -> + Any (not (tv `elemVarSet` bvs) && check_fv tv) + do_hole hole = do_tcv (coHoleCoVar hole) anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool anyFreeVarsOfType check_fv ty = DM.getAny (runFVTop (f ty)) ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -631,11 +631,13 @@ tcInstFun :: QLFlag -- plus the modification in Fig 5, of the QL paper: -- "A quick look at impredicativity" (ICFP'20). tcInstFun do_ql inst_final rn_head@(_, fun_lspan) tc_fun fun_sigma rn_args - = do { traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun + = do { lvl <- getTcLevel + ; traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun , text "rn_fun" <+> ppr rn_head , text "fun_sigma" <+> ppr fun_sigma , text "args:" <+> ppr rn_args - , text "do_ql" <+> ppr do_ql]) + , text "do_ql" <+> ppr do_ql + , text "lvl:" <+> ppr lvl ]) ; fun_origin <- mk_origin rn_head ; res@(_, fun_ty) <- go fun_origin 1 [] fun_sigma rn_args ; traceTc "tcInstFun:ret" (ppr fun_ty) @@ -1377,13 +1379,15 @@ tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty -- is not fully zonked, because ty_arg is fully zonked. -- See Note [Type application substitution]. + ; lvl <- getTcLevel ; traceTc "tc_inst_forall_arg (VTA/VDQ)" ( vcat [ text "fun_ty" <+> ppr fun_ty , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind , text "ty_arg" <+> debugPprType ty_arg <+> dcolon <+> debugPprType (typeKind ty_arg) , text "inner_ty" <+> debugPprType inner_ty - , text "insted_ty" <+> debugPprType insted_ty ]) + , text "insted_ty" <+> debugPprType insted_ty + , text "lvl:" <+> ppr lvl ]) ; return (ty_arg, insted_ty) } {- Note [Visible type application and abstraction] @@ -1934,11 +1938,13 @@ quickLookArg1 pos app_lspan rn_head larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_ -- capture and save it in the `EValArgQL`. See (QLA6) in -- Note [Quick Look at value arguments] + ; lvl <- getTcLevel ; traceTc "quickLookArg {" $ vcat [ text "arg:" <+> ppr arg , text "orig_arg_rho:" <+> ppr orig_arg_rho , text "head:" <+> ppr rn_fun_arg <+> dcolon <+> ppr mb_fun_ty - , text "args:" <+> ppr rn_args ] + , text "args:" <+> ppr rn_args + , text "level:" <+> ppr lvl ] ; case mb_fun_ty of { Nothing -> skipQuickLook app_lspan larg sc_arg_ty ; -- fun is too complicated @@ -2158,18 +2164,23 @@ qlUnify :: TcType -> TcType -> TcM () -- * It may return without having made the argument types equal, of course; -- it just makes best efforts. qlUnify ty1 ty2 - = do { traceTc "qlUnify" (ppr ty1 $$ ppr ty2) + = do { lvl <- getTcLevel + ; traceTc "qlUnify" (ppr lvl $$ ppr ty1 $$ ppr ty2) ; go ty1 ty2 } where go :: TcType -> TcType -> TcM () + go t1 t2 = do { traceTc "qlUinfy:go" (ppr t1 <+> char '~' <+> ppr t2) + ; go' t1 t2 } + -- Decompose (arg1 -> res1) ~ (arg2 -> res2) -- and (c1 => res1) ~ (c2 => res2) -- But for the latter we only learn instantiation info from res1~res2 - go (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 }) + go' (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 }) (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2 }) | af1 == af2 -- Match the arrow TyCon - = do { when (isVisibleFunArg af1) (go arg1 arg2) + = do { traceTc "go_fun" (ppr arg1 $$ ppr arg2) + ; when (isVisibleFunArg af1) (go arg1 arg2) -- NB: we do not unify the multiplicities; that would be too strong. -- We might only require mult1 ⩽ mult2, as in Note [Multiplicity in deep subsumption]. @@ -2178,30 +2189,30 @@ qlUnify ty1 ty2 ; go res1 res2 } -- Make sure to not unify "kappa := (a %1 -> b)". See (UQL5). - go (FunTy { ft_mult = OneTy }) _ = return () - go _ (FunTy { ft_mult = OneTy }) = return () + go' (FunTy { ft_mult = OneTy }) _ = return () + go' _ (FunTy { ft_mult = OneTy }) = return () -- NB: we do want to be able to unify "kappa := a => b", as that's -- the main point of QuickLook (allowing meta-variables to be unified -- with qualified types). - go (TyVarTy tv) ty2 + go' (TyVarTy tv) ty2 | isMetaTyVar tv = go_kappa tv ty2 - go ty1 (TyVarTy tv) + go' ty1 (TyVarTy tv) | isMetaTyVar tv = go_kappa tv ty1 - go (CastTy ty1 _) ty2 = go ty1 ty2 - go ty1 (CastTy ty2 _) = go ty1 ty2 + go' (CastTy ty1 _) ty2 = go ty1 ty2 + go' ty1 (CastTy ty2 _) = go ty1 ty2 - go (TyConApp tc1 []) (TyConApp tc2 []) + go' (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 -- See GHC.Tc.Utils.Unify = return () -- Note [Expanding synonyms during unification] -- Now, and only now, expand synonyms - go rho1 rho2 + go' rho1 rho2 | Just rho1 <- coreView rho1 = go rho1 rho2 | Just rho2 <- coreView rho2 = go rho1 rho2 - go (TyConApp tc1 tys1) (TyConApp tc2 tys2) + go' (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2 , not (isTypeFamilyTyCon tc1) , tys1 `equalLength` tys2 @@ -2209,14 +2220,14 @@ qlUnify ty1 ty2 -- Don't allow unifying (a => b) with the AppTy 'arr[tau] a b'. -- To ensure this, use 'tcSplitAppTyNoView_maybe' which does not split (=>). - go (AppTy t1a t1b) ty2 + go' (AppTy t1a t1b) ty2 | Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2 = do { go t1a t2a; go t1b t2b } - go ty1 (AppTy t2a t2b) + go' ty1 (AppTy t2a t2b) | Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1 = do { go t1a t2a; go t1b t2b } - go _ _ = return () + go' _ _ = return () -- Don't look under foralls; see (UQL4) of Note [QuickLook unification] ---------------- @@ -2244,7 +2255,11 @@ 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. + ; traceTc "go_flexi1" (ppr kappa $$ ppr ty2) ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of + -- qlUnify depends, regrettably delicately, on the exact choices made + -- by `simpleUnifyCheck`. See (SUC1) in + -- Note [simpleUnifyCheck] in GHC.Tc.Utils.Unify SUC_CanUnify -> do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind -- unifyKind: see (UQL2) in Note [QuickLook unification] @@ -2253,7 +2268,8 @@ qlUnify ty1 ty2 ; traceTc "qlUnify:update" $ ppr kappa <+> text ":=" <+> ppr ty2 ; liftZonkM $ writeMetaTyVar kappa ty2' } - _ -> return () -- e.g. occurs-check or forall-bound variable + suc -> do { traceTc "go_flexi2" (ppr suc $$ ppr kappa $$ ppr ty2) + ; return () } -- e.g. occurs-check or forall-bound variable } where kappa_kind = tyVarKind kappa ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -103,7 +103,6 @@ import GHC.Types.Id( idType ) import GHC.Types.Var as Var import GHC.Types.Var.Set import GHC.Types.Var.Env -import GHC.Types.Var.FV import GHC.Types.Basic import GHC.Types.Unique.Set (nonDetEltsUniqSet) @@ -120,7 +119,6 @@ import GHC.Data.Maybe (firstJusts) import Control.Monad import Data.Functor.Identity (Identity(..)) import qualified Data.List.NonEmpty as NE -import Data.Monoid as DM ( Any(..) ) import qualified Data.Semigroup as S ( (<>) ) import Data.Traversable (for) @@ -3143,6 +3141,7 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref, u_given_eq_lvl = given_eq_lvl }) do { traceTc "uUnfilledVar2 not ok" $ vcat [ text "tv1:" <+> ppr tv1 , text "ty2:" <+> ppr ty2 + , text "given_eq_lvl:" <+> ppr given_eq_lvl , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2) ] -- Occurs check or an untouchable: just defer @@ -3246,6 +3245,7 @@ lhsPriority tv ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Question: given a homogeneous equality (alpha ~# ty), when is it OK to unify alpha := ty? + (This note only applies to /homogeneous/ equalities, in which both sides have the same kind.) @@ -3354,6 +3354,14 @@ Needless to say, all there are wrinkles: GHC.Tc.Solver.floatEqualities, around Nov 2020. It's much easier to unify in-place, with no floating. +* (COERCIONS) What if there are coercions in the RHS? E.g. + alpha ~ (ty |> co) + or alpha ~ (ty co) + We only recurse into the `coercionType` of `co` rather than `co` itself. + Why? Mainly because `co` might be a coercion hole, in which case we /can't/ + recurse into the coercion that will eventually fill the hole. This came + up in #26543. + Note [TyVar/TyVar orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See also Note [Fundeps with instances, and equality orientation] @@ -3619,6 +3627,8 @@ simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUn -- unification might still be OK, but it'll take more work to do -- (use the full 'checkTypeEq'). -- +-- See Note [simpleUnifyCheck] +-- -- * Rejects if lhs_tv occurs in rhs_ty (occurs check) -- * Rejects foralls unless -- lhs_tv is RuntimeUnk (used by GHCi debugger) @@ -3638,10 +3648,7 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs | otherwise = SUC_NotSure where - lhs_info = metaTyVarInfo lhs_tv - - !(occ_in_ty, occ_in_co) = mkOccFolders (tyVarName lhs_tv) - + lhs_info = metaTyVarInfo lhs_tv lhs_tv_lvl = tcTyVarLevel lhs_tv lhs_tv_is_concrete = isConcreteTyVar lhs_tv @@ -3660,11 +3667,12 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs UC_OnTheFly -> False rhs_is_ok (TyVarTy tv) - | lhs_tv == tv = False - | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False - | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False - | occ_in_ty $! (tyVarKind tv) = False - | otherwise = True + | lhs_tv == tv = False -- Occurs check + | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False + | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False + | not (rhs_is_ok $! tyVarKind tv) = False + | otherwise = True + -- Hmm. We probably don't need the level check inside the kind, but no harm rhs_is_ok (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | not forall_ok, isInvisibleFunArg af = False @@ -3681,33 +3689,44 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs | otherwise = False rhs_is_ok (AppTy t1 t2) = rhs_is_ok t1 && rhs_is_ok t2 - rhs_is_ok (CastTy ty co) = not (occ_in_co co) && rhs_is_ok ty - rhs_is_ok (CoercionTy co) = not (occ_in_co co) + rhs_is_ok (CastTy ty co) = co_is_ok co && rhs_is_ok ty + rhs_is_ok (CoercionTy co) = co_is_ok co rhs_is_ok (LitTy {}) = True + -- For coercions we look only in the /type/ of the coercion + -- See (SUC1) in Note [simpleUnifyCheck] + co_is_ok co = rhs_is_ok (coercionType co) -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 --- No expansion of type synonyms -mkOccFolders lhs_tv = ( getAny . runFVTop . check_ty - , getAny . runFVTop . check_co) - where - check_ty :: Type -> FV BoundVars Any - !(check_ty, _, check_co, _) = foldTyCo occ_folder - - occ_folder :: TyCoFolder (FV BoundVars Any) - occ_folder = TyCoFolder { tcf_view = noView -- Don't expand synonyms - , tcf_tyvar = do_tcv, tcf_covar = do_tcv - , tcf_hole = do_hole - , tcf_tycobinder = addBndrFV } - - do_tcv v = (MkFV $ \ bvs -> - Any (not (v `elemVarSet` bvs) && tyVarName v == lhs_tv)) - `mappend` check_ty (varType v) - - do_hole _hole = MkFV $ \ _bvs -> DM.Any True -- Reject coercion holes +{- Note [simpleUnifyCheck] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +The function `simpleUnifyCheck` is asimple, /fast/ check for unifying (tv ~ rhs). +It can return a definite decision (SUC_CannotUnify of SUC_CanUnify), or uncertainty +(SUC_NotSure). In the latter case we will later use `checkTyEqRhs` to resolve. +In particular, `simpleUnifyCheck`: + +* Rejects if lhs_tv occurs in rhs_ty (occurs check) +* Rejects foralls unless + lhs_tv is RuntimeUnk (used by GHCi debugger) + or is a QL instantiation variable +* Rejects a non-concrete type if lhs_tv is concrete +* Rejects type families unless fam_ok=True +* Does a level-check for type variables, to avoid skolem escape + +This function is pretty heavily used, so it's optimised not to allocate. + +(SUC1) `simpleUnifyCheck` used by QuickLook's `qlUnify`, and anything other than + SUC_CanUnify will tell `qlUnify` not to proceed. That makes QuickLook depend + (regrettably, delicately) on the exact choices made by `simpleUnifyCheck`. + + A case in point: in #26543. In the repro case in the Descriptions, `qlUnify` failed + because there was a coercion hole in the RHS; but one that was ultimately Refl. + + So we only look at the /kind/ of a coercion, not the evidence itself. I'm a bit + worried about building a loop, if the evidence mentions the LHS unification + variable; but I can't see how that can happen, and I /really/ don't want to be + super-conservative for coercion holes (#26543). So, for now at least, we look + just at the kind of the coercion. +-} {- ********************************************************************* * * @@ -4337,7 +4356,11 @@ checkCo flags co = -- Occurs check (can promote) | OC_Check lhs_tv occ_prob <- occ , LC_Promote { lc_lvlp = lhs_tv_lvl } <- lc - -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co) + -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl $ + tyCoVarsOfCo co + -- Maybe we should just check the free vars of the + -- /type/ of the coercion, to line up with + -- (SUC1) in Note [simpleUnifyCheck] ; return $ if cterHasNoProblem reason then pure co @@ -4697,12 +4720,14 @@ simpleOccursCheck :: OccursCheck -> TcTyVar -> TyVarCheckResult m simpleOccursCheck OC_None _ = TyVarCheck_Success simpleOccursCheck (OC_Check lhs_tv occ_prob) occ_tv - | lhs_tv == tyVarName occ_tv || check_kind (tyVarKind occ_tv) - = TyVarCheck_Error (cteProblem occ_prob) - | otherwise - = TyVarCheck_Success + | check_fv occ_tv = TyVarCheck_Error (cteProblem occ_prob) + | otherwise = TyVarCheck_Success where - (check_kind, _) = mkOccFolders lhs_tv + check_fv :: TyCoVar -> Bool -- True <=> occurs check + check_fv occ_tcv + | lhs_tv == tyVarName occ_tcv = True + | anyFreeVarsOfType check_fv (tyVarKind occ_tcv) = True + | otherwise = False ------------------------- tyVarLevelCheck :: LevelCheck m -> TcTyVar -> TyVarCheckResult m ===================================== testsuite/tests/typecheck/should_compile/T26543_orig.hs ===================================== @@ -0,0 +1,36 @@ +-- This test is from the Description of #26543 + +{-# LANGUAGE GHC2024, TypeAbstractions, AllowAmbiguousTypes, NoImplicitPrelude, + TypeFamilies, UndecidableInstances #-} +module T26543_orig where + +import Data.Kind +import Control.Applicative (Applicative(..)) +import Prelude (type (~), ($)) + +type CAT k = k -> k -> Type + +type family (~>) :: CAT k +type family Ob (a :: k) :: Constraint +type family UN (w :: j -> k) (wa :: k) :: j + +class HasBinaryProducts k where + type (a :: k) && (b :: k) :: k + withObProd :: (Ob (a :: k), Ob b) => ((Ob (a && b)) => r) -> r + (&&&) :: ((a :: k) ~> x) -> (a ~> y) -> (a ~> (x && y)) + +data AP (f :: Type -> Type) k = A k +type instance UN A (A k) = k + +type Ap :: CAT (AP f k) +data Ap a b where + Ap :: forall {k} a b f. (Ob a, Ob b) => f (a ~> b) -> Ap (A a :: AP f k) (A b) + +type instance (~>) = Ap +type instance Ob a = (a ~ A (UN A a), Ob (UN A a)) + +instance (Applicative f, HasBinaryProducts k) => HasBinaryProducts (AP f k) where + type a && b = A (UN A a && UN A b) + withObProd @(A a) @(A b) r = withObProd @k @a @b r + -- (&&&) :: Ap (a :: AP f k) x -> Ap a y -> Ap a (x && y) + Ap @_ @x f &&& Ap @_ @y g = withObProd @k @x @y $ Ap (liftA2 (&&&) f g) ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -969,3 +969,4 @@ test('ExpansionQLIm', normal, compile, ['']) test('T23135', normal, compile, ['']) test('LazyFieldAnnotations', normal, compile, ['']) test('T27557', normal, compile, ['']) +test('T26543_orig', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/defc3eae2fd24582516f77f4beab0a31... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/defc3eae2fd24582516f77f4beab0a31... You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help