Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC Commits: a4233abb by Simon Peyton Jones at 2026-09-29T00:07:46+01:00 Final wibbles .. still need a decent commit message - - - - - 6 changed files: - compiler/GHC/Runtime/Heap/Inspect.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Runtime/Heap/Inspect.hs ===================================== @@ -630,7 +630,7 @@ be sigmas and not taus. ~~~~~~~~~~~~~~~~~~~~~~ In the GHCi debugger we use unification variables whose MetaInfo is RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can -unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq). +unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification). If we don't do this `:print <term>` will fail if the type of <term> has nested `forall`s or `=>`s. ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -21,6 +21,7 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin +import GHC.Tc.Types( TcM ) import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe ) @@ -36,8 +37,8 @@ import GHC.Core.Coercion import GHC.Core.Reduction import GHC.Core.FamInstEnv ( FamInstEnvs ) import GHC.Core -import GHC.Types.Var +import GHC.Types.Var import GHC.Types.Basic import GHC.Types.Name.Reader import GHC.Types.Var.Env @@ -49,6 +50,8 @@ import GHC.Utils.Misc import GHC.Utils.Monad import GHC.Data.Pair +import GHC.Data.Bag + import Control.Monad import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) @@ -2257,7 +2260,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs else rewriteEqEvidence ev swapped (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn emptyCoHoleSet - -- emptyCoHoleSet: rhs_redn has no CoercionHoles + -- emptyCoHoleSet: we are about to /solve/ this + -- constraint, so its CoHoleSet doesn't matter ; let tv_ty = mkTyVarTy tv final_rhs = reductionReducedType rhs_redn @@ -2285,21 +2289,12 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs -- We can't unify, but we can see if this equality can go in the inert set -- and be used to rewrite other constraints. -- See Note [Equalities where unification fails] - = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F) + = do { -- Do checkTypeEqNoUnfication to guarantee (TyEq:OC), (TyEq:F) -- Must do the occurs check even on tyvar/tyvar equalities, -- in case have x ~ (y :: ..x...); this is #12593. - ; check_result <- checkTypeEq ev eq_rel lhs rhs + ; check_result <- checkTypeEqNoUnification ev eq_rel lhs rhs ; case check_result of PuFail reason -{- - | reason `cterHasOnlyProblems` do_not_prevent_rewriting - -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs - ; continueWith $ Right $ - EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs , eq_rhs = rhs } } - - | otherwise --} -> -- We can't unify, and this equality should not be used to rewrite -- other constraints (e.g. because it has an occurs check). -- So add it to the inert Irreds. @@ -2307,19 +2302,27 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs ; finishCanWithIrred (NonCanonicalReason reason) new_ev } PuOK new_eqs rhs_redn - -> -- Claim: there should be no new_eqs - -- The non-unification check does non promotion nor type-family - -- flattening for Wanteds + -> -- Put this constraint into the inert set, so that it will be used + -- to solve or rewrite other constraints. + -- + -- NB: checkTypeEqNoUnification does not check for + -- (b) skolem-escape (tefTyVar_levelCheck = LC_None) + -- (a) concreteness (tefTyVar_concreteCheck = CC_None) + -- So an equality whose only problem is e.g. skolem-escape will + -- return PuOK, will be put in the inert set, will be used for + -- rewriting. That is fine. + -- + -- assertPpr (isEmptyCts new_eqs): + -- checkTypeEqNoUnification does neither promotion nor type-family + -- flattening for Wanteds, and hence creates no equalities to solve assertPpr (isEmptyCts new_eqs) (vcat [ text "new_eqs" <+> ppr new_eqs , text "rhs_redn" <+> ppr rhs_redn , text "lhs" <+> ppr lhs , text "rhs" <+> ppr rhs ]) $ - do { emitWork new_eqs - ; let new_holes = rewriterSetFromCts new_eqs - lhs_ty = canEqLHSType lhs + do { let lhs_ty = canEqLHSType lhs lhs_redn = mkReflRedn (eqRelRole eq_rel) lhs_ty - ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes + ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn emptyCoHoleSet -- Important: even if the coercion is Refl, -- * new_ev has reductionReducedType on the RHS @@ -2330,19 +2333,54 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs , eq_lhs = lhs , eq_rhs = reductionReducedType rhs_redn } } } -{- --- | Some problems prevent /unification/ but not /rewriting/: --- --- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3] --- we can't unify (skolem-escape); but it /is/ canonical, --- and hence we /can/ use it for rewriting --- --- Concrete-ness: alpha[conc] ~ b[sk] --- We can use it to rewrite; we still have to solve the original -do_not_prevent_rewriting :: CheckTyEqResult -do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> - cteProblem cteConcrete --} +checkTypeEqNoUnification :: CtEvidence -> EqRel -> CanEqLHS -> TcType + -> TcS (PuResult Ct Reduction) +-- Used for general CanEqLHSs, when we have decided that we cannot unify +checkTypeEqNoUnification ev eq_rel lhs rhs = + case ev of + CtGiven {} -> + do { traceTcS "checkTypeEqNoUnification (given) {" (vcat [ text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ]) + ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs) + ; traceTcS "checkTypeEqNoUnification }" (ppr check_result) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs + ; emitWork new_givens + ; updInertSet (addCycleBreakerBindings prs) + ; return (pure redn) } } + CtWanted {} -> do { traceTcS "checkTypeEqNoUnification (wanted) {" $ + vcat [ text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ] + ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) + ; traceTcS "checkTypeEqNoUnification }" (ppr check_result) + ; return check_result } + where + wanted_flags :: TyEqFlags TcM Ct + wanted_flags = notUnifying_TEFTask occ_prob lhs + -- See Note [Don't cycle-break Wanteds when not unifying] + + given_flags :: TyEqFlags TcM (TcTyVar, TcType) + given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven } + -- TEFA_Break used for: [G] a ~ Maybe (F a) + -- or [G] F a ~ Maybe (F a) + + -- occ_prob: see Note [Occurs check and representational equality] + occ_prob = case eq_rel of + NomEq -> cteInsolubleOccurs + ReprEq -> cteSolubleOccurs + + --------------------------- + mk_new_given :: (TcTyVar, TcType) -> TcS Ct + mk_new_given (new_tv, fam_app) + = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term) + where + new_ty = mkTyVarTy new_tv + given_pred = mkNomEqPred fam_app new_ty + given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note + + -- See Detail (7) of the Note + cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin ---------------------- finishCanWithIrred :: CtIrredReason -> CtEvidence @@ -2371,16 +2409,53 @@ inert set so that it can be used to rewrite other Wanteds. (There are many reasons by unification might not happen: the LHS is not a touchable unification variable, it has rewriters, it's a Given etc.) -* In this case we call `checkTypeEq`to see if it is canonical (which in turn - calls `checkTypeEqRhs`). +* In this case we call `checkTypeEqNoUnification`to see if it is canonical (which + in turn calls `checkTypeEqRhs` with suitable flags). -* Even if `checkTypeEq` returns `PuFail`, we may /still/ be able to add it to the inert - set, depending on the reason for failure; examples are given in `do_not_prevent_rewriting`. +* NB: we do /not/ try to take advantage of the case where + `canEqCanLHSFinish_try_unification` has already called `checkTyEqRhs`; doing so + caused #27844. (The first call did fam-app breaking, which concealed a genuine + occurs check.) It's just too clever; better to do the simple thing. -* NB: we do /not/ try to take advantage of the case where `canEqCanLHSFinish_try_unification` - has already called `checkTyEqRhs`; doing so caused #27844. (The first call did fam-app - breaking, which concealed a genuine occurs check.) It's just too clever; better to do - the simple thing. +Note [Don't cycle-break Wanteds when not unifying] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consdier + [W] a[2] ~ Maybe (F a[2]) + +Should we cycle-break this Wanted, thus? + + [W] a[2] ~ Maybe delta[2] + [W] delta[2] ~ F a[2] + +For a start, this is dodgy because we might just unify delta, thus undoing +what we have done, and getting an infinite loop in the solver. Even if we +somehow prevented ourselves from doing so, is there any merit in the split? +Maybe: perhaps we can use that equality on `a` to unlock other constraints? +Consider + type instance F (Maybe _) = Bool + + [G] g1: a ~ Maybe Bool + [W] w1: a ~ Maybe (F a) + +If we loop-break w1 to get + [W] w1': a ~ Maybe gamma + [W] w3: gamma ~ F a +Now rewrite w3 with w1' + [W] w3': gamma ~ F (Maybe gamma) +Now use the type instance to get + gamma := Bool +Now we are left with + [W] w1': a ~ Maybe Bool +which we can solve from the Given. + +BUT in this situation we could have rewritten the +/original/ Wanted from the Given, like this: + [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool)) +and that is readily soluble. + +In short: loop-breaking Wanteds, when we aren't unifying, +seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break, +in `wanted_flags` in `checkTypeEqNoUnification`. Note [Equalities with heterogeneous kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2565,8 +2640,7 @@ The details depend on whether we're working with a Given or a Wanted. Given ----- We emit a new Given, [G] F a ~ cbv, equating the type family application -to our new cbv. This is actually done by `break_given` in -`GHC.Tc.Solver.Monad.checkTypeEq`. +to our new cbv. This is actually done by `break_given` in `checkTypeEqNoUnification`. Note its orientation: The type family ends up on the left; see Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -983,7 +983,7 @@ How do we establish these conditions? with S(fw,_). * (T3) is guaranteed by an occurs-check on the work item. - This is done during canonicalisation, in checkTypeEq; invariant + This is done during canonicalisation, in checkTyEqRhs; invariant (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint. * (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable. If the inert ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -117,10 +117,7 @@ module GHC.Tc.Solver.Monad ( getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, matchFam, matchFamTcM, checkWellLevelledDFun, - pprEq, - - -- Enforcing invariants for type equalities - checkTypeEq + pprEq ) where import GHC.Prelude @@ -2302,57 +2299,6 @@ wrapUnifier rws loc role do_unifications ************************************************************************ -} -checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType - -> TcS (PuResult Ct Reduction) --- Used for general CanEqLHSs, ones that do --- not have a touchable type variable on the LHS (i.e. not unifying) -checkTypeEq ev eq_rel lhs rhs = - case ev of - CtGiven {} -> - do { traceTcS "checkTypeEq (given) {" (vcat [ text "lhs:" <+> ppr lhs - , text "rhs:" <+> ppr rhs ]) - ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs) - ; traceTcS "checkTypeEq }" (ppr check_result) - ; case check_result of - PuFail reason -> return (PuFail reason) - PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs - ; emitWork new_givens - ; updInertSet (addCycleBreakerBindings prs) - ; return (pure redn) } } - CtWanted {} -> do { traceTcS "checkTypeEq (wanted) {" $ - vcat [ text "lhs:" <+> ppr lhs - , text "rhs:" <+> ppr rhs ] - ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) - ; traceTcS "checkTypeEq }" (ppr check_result) - ; return check_result } - where - wanted_flags :: TyEqFlags TcM Ct - wanted_flags = notUnifying_TEFTask occ_prob lhs - -- checkTypeEq deals only with the non-unifying case - - given_flags :: TyEqFlags TcM (TcTyVar, TcType) - given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven } - -- TEFA_Break used for: [G] a ~ Maybe (F a) - -- or [G] F a ~ Maybe (F a) - - -- occ_prob: see Note [Occurs check and representational equality] - occ_prob = case eq_rel of - NomEq -> cteInsolubleOccurs - ReprEq -> cteSolubleOccurs - - --------------------------- - mk_new_given :: (TcTyVar, TcType) -> TcS Ct - mk_new_given (new_tv, fam_app) - = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term) - where - new_ty = mkTyVarTy new_tv - given_pred = mkNomEqPred fam_app new_ty - given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note - - -- See Detail (7) of the Note - cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin - -------------------------- -- | Fill in CycleBreakerTvs with the variables they stand for. -- See Note [Type equality cycles] in GHC.Tc.Solver.Equality restoreTyVarCycles :: InertSet -> TcM () @@ -2368,43 +2314,4 @@ restoreTyVarCycles is (a ~R# b a) is soluble if b later turns out to be Identity So we treat this as a "soluble occurs check". -Note [Don't cycle-break Wanteds when not unifying] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consdier - [W] a[2] ~ Maybe (F a[2]) - -Should we cycle-break this Wanted, thus? - - [W] a[2] ~ Maybe delta[2] - [W] delta[2] ~ F a[2] - -For a start, this is dodgy because we might just unify delta, thus undoing -what we have done, and getting an infinite loop in the solver. Even if we -somehow prevented ourselves from doing so, is there any merit in the split? -Maybe: perhaps we can use that equality on `a` to unlock other constraints? -Consider - type instance F (Maybe _) = Bool - - [G] g1: a ~ Maybe Bool - [W] w1: a ~ Maybe (F a) - -If we loop-break w1 to get - [W] w1': a ~ Maybe gamma - [W] w3: gamma ~ F a -Now rewrite w3 with w1' - [W] w3': gamma ~ F (Maybe gamma) -Now use the type instance to get - gamma := Bool -Now we are left with - [W] w1': a ~ Maybe Bool -which we can solve from the Given. - -BUT in this situation we could have rewritten the -/original/ Wanted from the Given, like this: - [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool)) -and that is readily soluble. - -In short: loop-breaking Wanteds, when we aren't unifying, -seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break, -in `wanted_flags` in `checkTypeEq`. -} ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -524,7 +524,7 @@ isInsolubleReason (InsolubleFunDepReason {}) = True ------------------------------------------------------------------------------ -- | A /set/ of problems in checking the validity of a type equality. --- See 'checkTypeEq'. +-- See 'GHC.Tc.Utils.Unify.checkTyEqRhs'. newtype CheckTyEqResult = CTER Word8 -- | No problems in checking the validity of a type equality. ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3617,7 +3617,7 @@ instance Outputable SimpleUnifyResult where simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUnifyResult -- ^ A fast check for unification. May return "not sure", in which case -- unification might still be OK, but it'll take more work to do --- (use the full 'checkTypeEq'). +-- (use the full 'checkTyEqRhs'). -- -- It returns SUC_CannotUnify for -- * Touchability failure @@ -4289,7 +4289,7 @@ NB: We never see a TyVarLHS here, such as [G] a ~ F tys here because we'd have swapped it to [G] F tys ~ a -in canEqCanLHS2, before getting to checkTypeEq. +in canEqCanLHS2, before getting to checkTyEqRhs. -} check_ty_eq_rhs :: forall m a @@ -4813,7 +4813,6 @@ promote_meta_tyvar info dest_lvl occ_tv touchabilityTest :: TcLevel -> TcTyVar -> Bool -- ^ This is the key test for untouchability: -- See Note [Unification preconditions] in GHC.Tc.Utils.Unify --- and Note [Solve by unification] in GHC.Tc.Solver.Equality -- -- @True@ <=> the variable is touchable touchabilityTest given_eq_lvl tv View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a4233abb501f48b8f359a2af0dc1fc64... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a4233abb501f48b8f359a2af0dc1fc64... 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