Simon Peyton Jones pushed to branch wip/T26543b at Glasgow Haskell Compiler / GHC Commits: 5e6c1f43 by Simon Peyton Jones at 2026-10-01T13:07:42+01:00 Rename CycleBreakerTv to GivenCycleBreakerTv [skip ci] .. and add documentation - - - - - 7 changed files: - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -2584,15 +2584,15 @@ turn controls the behaviour of the workhorse: GHC.Tc.Utils.Unify.checkTyEqRhs. The details depend on whether we're working with a Given or a Wanted. -Given ------ +Note [Type equality cycles: Givens] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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`. -Note its orientation: The type family ends up on the left; see -Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for -CycleBreakerTvs is necessary. This scenario is now easily soluble, by using +Note its orientation: The type family ends up on the left; +see Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for +GivenCycleBreakerTvs is necessary. This scenario is now easily soluble, by using the first Given to rewrite the Wanted, which can now be solved. (The first Given actually also rewrites the second one, giving @@ -2613,10 +2613,11 @@ to Note that * `cbv` is a fresh cycle breaker variable. -* `cbv` is a meta-tyvar, but it is completely untouchable. +* `cbv` is a meta-tyvar, of flavour GivenCycleBreakerTv, but it is + completely untouchable. * We track the cycle-breaker variables in inert_cycle_breakers in InertSet -* We eventually fill in the cycle-breakers, with `cbv := F lhs`. - No one else fills in CycleBreakerTvs! +* We eventually fill in the cycle-breakers, with `cbv := F lhs`, + via `restoreTyVarCycles`. No one else fills in GivenCycleBreakerTvs! * The evidence for the new `F lhs ~ cbv` constraint is Refl, because we know this fill-in is ultimately going to happen. * In `inert_cycle_breakers`, we remember the (cbv, F lhs) pair; that is, we @@ -2626,8 +2627,8 @@ Note that * This fill-in is done when solving is complete, by restoreTyVarCycles in nestImplicTcS and runTcSWithEvBinds. -Wanted ------- +Note [Type equality cycles: Wanteds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ First, we do not cycle-break unless the LHS is a unifiable type variable See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad. @@ -2686,9 +2687,9 @@ to unify the cbvs: [W] AllEqF '[Bool] alpha Without the logic detailed in this Note, we're stuck here, as AllEqF cannot -reduce and alpha cannot unify. Let's instead apply our cycle-breaker approach, -just as described above. We thus invent cbv1 and cbv2 and unify -alpha := cbv1 -> cbv2, yielding (after zonking) +reduce and alpha cannot unify (occurs check). Let's instead apply our +cycle-breaker approach, just as described above. We thus invent cbv1 and cbv2 +and unify alpha := (cbv1 : cbv2), yielding (after zonking) [W] Head (cbv1 : cbv2) ~ cbv1 [W] Tail (cbv1 : cbv2) ~ cbv2 @@ -2726,8 +2727,8 @@ Note that we need to unify the cbvs here; if we did not, there would be no way to solve those constraints. That's why the cycle-breakers are ordinary TauTvs. -How all this is implemented ---------------------------- +Note [Type equality cycles: implementation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We implement all this via the `TEFA_Break` constructor of `TyEqFamApp`, itself stored in the `tef_fam_app` field of `TyEqFlags`, which controls the behaviour of `GHC.Tc.Utils.Unify.checkTyEqRhs`. The `TEFA_Break` @@ -2854,7 +2855,7 @@ More details: CycleBreakerOrigin. This works for both Givens and Wanteds, as we need the logic in the W case for e.g. typecheck/should_fail/T17139. Because this logic needs to work for Wanteds, too, we cannot simply look for a - CycleBreakerTv on the left: Wanteds don't use them. + GivenCycleBreakerTv on the left: Wanteds don't use them. ********************************************************************** ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -304,7 +304,7 @@ instance Outputable WorkList where ********************************************************************* -} type CycleBreakerVarStack = NE.NonEmpty (Bag (TcTyVar, TcType)) - -- ^ a stack of (CycleBreakerTv, original family applications) lists + -- ^ A stack of (GivenCycleBreakerTv, original family applications) lists -- first element in the stack corresponds to current implication; -- later elements correspond to outer implications -- used to undo the cycle-breaking needed to handle @@ -324,6 +324,8 @@ data InertSet -- See `resetInertCans` , inert_cycle_breakers :: CycleBreakerVarStack + -- The equalities for /given/ cycle breakers, GivenCycleBreakerTvs + -- See Note [ , inert_famapp_cache :: FunEqMap Reduction -- Just a hash-cons cache for use when reducing family applications @@ -1942,7 +1944,8 @@ prohibitedSuperClassSolve given_loc wanted_loc {- ********************************************************************* * * - Cycle breakers + Given Cycle breakers + See Note [Type equality cycles: Givens] in GHC.Tc.Solver.Equality * * ********************************************************************* -} ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -2344,12 +2344,12 @@ checkTypeEq ev eq_rel lhs rhs = given_pred = mkNomEqPred fam_app new_ty given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note - -- See Detail (7) of the Note + -- See Detail (7) of Note [Type equality cycles: implementation] 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 +-- See Note [Type equality cycles: Givens] in GHC.Tc.Solver.Equality restoreTyVarCycles :: InertSet -> TcM () restoreTyVarCycles is = TcM.liftZonkM ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -726,11 +726,11 @@ cloneMetaTyVarName name metaInfoToTyVarName :: MetaInfo -> FastString metaInfoToTyVarName meta_info = case meta_info of - TauTv -> fsLit "t" - TyVarTv -> fsLit "a" - RuntimeUnkTv -> fsLit "r" - CycleBreakerTv -> fsLit "b" - ConcreteTv {} -> fsLit "c" + TauTv -> fsLit "t" + TyVarTv -> fsLit "a" + RuntimeUnkTv -> fsLit "r" + GivenCycleBreakerTv -> fsLit "b" + ConcreteTv {} -> fsLit "c" newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi @@ -824,7 +824,7 @@ cloneAnonMetaTyVar info tv kind -- in GHC.Tc.Solver.Equality. newCycleBreakerTyVar :: TcKind -> TcM TcTyVar newCycleBreakerTyVar kind - = do { details <- newMetaDetails CycleBreakerTv + = do { details <- newMetaDetails GivenCycleBreakerTv ; name <- newMetaTyVarName (fsLit "cbv") ; return (mkTcTyVar name kind details) } ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -688,9 +688,10 @@ data MetaInfo | RuntimeUnkTv -- ^ A unification variable used in the GHCi debugger. -- It /is/ allowed to unify with a polytype, unlike TauTv - | CycleBreakerTv -- ^ Used to fix occurs-check problems in Givens - -- See Note [Type equality cycles] in - -- GHC.Tc.Solver.Equality + | GivenCycleBreakerTv -- ^ Used to fix occurs-check problems in Givens + -- Never used for Wanteds + -- See Note [Type equality cycles] in + -- GHC.Tc.Solver.Equality | ConcreteTv ConcreteTvOrigin -- ^ A unification variable that can only be unified @@ -705,11 +706,11 @@ instance Outputable MetaDetails where ppr (Indirect ty) = text "Indirect" <+> ppr ty instance Outputable MetaInfo where - ppr TauTv = text "tau" - ppr TyVarTv = text "tyv" - ppr RuntimeUnkTv = text "rutv" - ppr CycleBreakerTv = text "cbv" - ppr (ConcreteTv {}) = text "conc" + ppr TauTv = text "tau" + ppr TyVarTv = text "tyv" + ppr RuntimeUnkTv = text "rutv" + ppr GivenCycleBreakerTv = text "cbv" + ppr (ConcreteTv {}) = text "conc" -- | What caused us to create a 'ConcreteTv' metavariable? -- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete. @@ -1299,7 +1300,7 @@ isRuntimeUnkTyVar tv isCycleBreakerTyVar tv | isTyVar tv -- See Note [Coercion variables in free variable lists] - , MetaTv { mtv_info = CycleBreakerTv } <- tcTyVarDetails tv + , MetaTv { mtv_info = GivenCycleBreakerTv } <- tcTyVarDetails tv = True | otherwise @@ -1350,8 +1351,8 @@ metaTyVarInfo tv isTouchableInfo :: MetaInfo -> Bool isTouchableInfo info - | CycleBreakerTv <- info = False - | otherwise = True + | GivenCycleBreakerTv <- info = False + | otherwise = True metaTyVarTcLevel :: TcTyVar -> TcLevel metaTyVarTcLevel tv ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3235,11 +3235,11 @@ lhsPriority tv -> 5 -- Eliminate instantiation variables first | otherwise -> case info of - CycleBreakerTv -> 0 - TyVarTv -> 1 - ConcreteTv {} -> 2 - TauTv -> 3 - RuntimeUnkTv -> 4 + GivenCycleBreakerTv -> 0 + TyVarTv -> 1 + ConcreteTv {} -> 2 + TauTv -> 3 + RuntimeUnkTv -> 4 {- Note [Unification preconditions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -3285,7 +3285,7 @@ There are five reasons not to unify: structured type. So if 'ty' is a structured type, such as (Maybe x), don't unify. - * CycleBreakerTv: never unified, except by restoreTyVarCycles. + * GivenCycleBreakerTv: never unified, except by restoreGivenCycles. 4. (CONCRETE) A ConcreteTv can only unify with a concrete type, by definition. @@ -3390,7 +3390,7 @@ So we look for a positive reason to swap, using a three-step test: touchable and can be unified. Tie-breaking rules for MetaTvs: - - CycleBreakerTv: This is essentially a stand-in for another type; + - GivenCycleBreakerTv: This is essentially a stand-in for another type; it's untouchable and should have the same priority as a skolem: 0. - TyVarTv: These can unify only with another tyvar, but we can't unify @@ -4112,13 +4112,14 @@ wantConcreteCheck = \case -- where @cbv@ is a fresh loop-breaker tyvar (for Given), or -- just a fresh 'TauTv' (for Wanted) famAppBreaker :: FamAppBreaker a -> TcType -> TcM (PuResult a Reduction) -famAppBreaker BreakGiven fam_app +famAppBreaker BreakGiven fam_app -- Givens = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app) ; return (PuOK (unitBag (new_tv, fam_app)) (mkReflRedn Nominal (mkTyVarTy new_tv))) } -- Why reflexive? See Detail (4) of Note [Type equality cycles] -- in GHC.Tc.Solver.Equality -famAppBreaker (BreakWanted ev lhs_tv) fam_app + +famAppBreaker (BreakWanted ev lhs_tv) fam_app -- Wanteds -- Occurs check or skolem escape; so flatten = do { reason <- checkPromoteFreeVars cteInsolubleOccurs (tyVarName lhs_tv) lhs_tv_lvl @@ -4861,7 +4862,7 @@ checkTopShape info xi RuntimeUnk -> True MetaTv { mtv_info = TyVarTv } -> True _ -> False - CycleBreakerTv -> False -- We never unify these + GivenCycleBreakerTv -> False -- We never unify these _ -> True -------------------------------------------------------------------------------- @@ -5174,14 +5175,14 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars -- (as they can be unified) - -- and also for CycleBreakerTvs that mentions meta-tyvars + -- and also for GivenCycleBreakerTvs that mentions meta-tyvars mentions_meta_ty_var :: TyVar -> Bool mentions_meta_ty_var tv | isMetaTyVar tv = case metaTyVarInfo tv of -- See Examples 8 and 9 in the Note - CycleBreakerTv -> anyFreeVarsOfType mentions_meta_ty_var - (lookupCycleBreakerVar tv inert_set) + GivenCycleBreakerTv -> anyFreeVarsOfType mentions_meta_ty_var + (lookupCycleBreakerVar tv inert_set) _ -> True | otherwise = False @@ -5224,7 +5225,7 @@ We want to solve w1 using g1 and g2. The presence of g3 is irrelevant, because we cannot unify 'f[tau:1] v[tau:1]' and 'g[sk:1] x[sk:3]' due to skolem escape. -} --- | Return the type family application a CycleBreakerTv maps to. +-- | Return the type family application a GivenCycleBreakerTv maps to. lookupCycleBreakerVar :: TcTyVar -- ^ cbv, must be a CycleBreakerTv -> InertSet -> TcType -- ^ type family application the cbv maps to ===================================== testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs ===================================== @@ -22,7 +22,7 @@ it mentions b in its RHS. It thus triggers Note [Type equality cycles] in GHC.Tc.Solver.Equality. That Note says we change the situation to [G] b ~ cbv GhcPs [G] Body b ~ cbv -for some fresh CycleBreakerTv cbv. Now, our original equality looks to be let-like, +for some fresh GivenCycleBreakerTv cbv. Now, our original equality looks to be let-like, but the new cbv equality is *not* let-like -- note that the variable is on the RHS. The solution is to consider any equality whose free variables are all at the current level to not stop equalities from floating. These are called *local*. Because both View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e6c1f43db2598cddfa54d909e2437dd... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e6c1f43db2598cddfa54d909e2437dd... 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