Simon Peyton Jones pushed to branch wip/T25440 at Glasgow Haskell Compiler / GHC Commits: 4d2a3dbc by Simon Peyton Jones at 2025-04-21T23:42:54+01:00 Improve comments following dicsussion with Richard And materially change canEqLHSHetero, so that it puts the constraint directly in the Irreds - - - - - 5 changed files: - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Zonk/TcType.hs Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1604,7 +1604,7 @@ canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2) -> TcType -> TcType -- xi2 -> TcKind -- ki2 -> TcS (StopOrContinue (Either IrredCt EqCt)) -canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 +canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 _ps_xi2 ki2 -- See Note [Equalities with incompatible kinds] -- See Note [Kind Equality Orientation] @@ -1625,6 +1625,9 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 -- Otherwise we might put something in the inert set that isn't inert then startAgainWith (mkNonCanonical ev) else + assertPpr (not (isEmptyRewriterSet rewriters)) (ppr ev) $ + -- The rewriter set won't be empty because the two kinds differ, and there + -- are no unifications, so we must have emitted one or more constraints do { let lhs_redn = mkReflRedn role ps_xi1 rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co mb_sym_kind_co = case swapped of @@ -1636,8 +1639,11 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn - ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co - ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }} + -- The rewritten equality is non-canonical, so put it straight in the Irreds + ; finishCanWithIrred (NonCanonicalReason (cteProblem cteCoercionHole)) type_ev } } + +-- ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co +-- ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }} where mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool) @@ -2044,19 +2050,20 @@ What do we do when we have an equality where k1 and k2 differ? Easy: we create a coercion that relates k1 and k2 and use this to cast. To wit, from - [X] (tv :: k1) ~ (rhs :: k2) + [X] co1 :: (tv :: k1) ~ (rhs :: k2) (where [X] is [G] or [W]), we go to - [X] co :: k1 ~ k2 - [X] (tv :: k1) ~ ((rhs |> sym co) :: k1) + co1 = co2 ; sym (GRefl kco) + [X] co2 :: (tv :: k1) ~ ((rhs |> sym kco) :: k1) + [X] kco :: k1 ~ k2 Wrinkles: -(EIK1) When X is W, the new type-level wanted is effectively rewritten by the - kind-level one. We thus include the kind-level wanted in the RewriterSet - for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. - This is done in canEqCanLHSHetero. +(EIK1) When X=Wanted, the new type-level wanted for `co` is effectively rewritten by + the kind-level one. We thus include the kind-level wanted in the RewriterSet + for the type-level one. See Note [Wanteds rewrite Wanteds] in + GHC.Tc.Types.Constraint. This is done in canEqCanLHSHetero. (EIK2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce [W] w : a ~ (b |> kw) @@ -2076,7 +2083,7 @@ Wrinkles: Instead, it lands in the inert_irreds in the inert set, awaiting solution of that `kw`. - (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets + (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets solved. This is done in `kickOutAfterFillingCoercionHole`, which kicks out all equalities whose RHS mentions the filled-in coercion hole. Note that it looks for type family equalities, too, because of the use of unifyTest @@ -2086,7 +2093,7 @@ Wrinkles: which records that `w` has been rewritten by `kw`. See (WRW3) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. - (EIK2b) What if the RHS mentions /other/ coercion holes? How can that happen? The + (EIK2b) What if the RHS mentions /other/ coercion holes? How can that happen? The main way is like this. Assume F :: forall k. k -> Type [W] kw : k ~ Type [W] w : a ~ F k t @@ -2097,15 +2104,32 @@ Wrinkles: rewriting. Indeed tests JuanLopez only typechecks if we do. So we'd like to treat this kind of equality as canonical. - Hence the ch_hetero_kind field in CoercionHole: it is True of constraints - created by `canEqCanLHSHetero` to fix up hetero-kinded equalities; and False otherwise: + So here is our implementation: + * The `ch_hetero_kind` field in CoercionHole identifies a coercion hole created + by `canEqCanLHSHetero` to fix up hetero-kinded equalities. * An equality constraint is non-canonical if it mentions a hetero-kind - CoercionHole on the RHS. See the `hasCoercionHoleCo` test in GHC.Tc.Utils.checkCo. + CoercionHole on the RHS. This (and only this) is the (TyEq:CH) invariant + for canonical equalities (see Note [Canonical equalities]) + + * The invariant is checked by See the `hasCoercionHoleCo` test in + GHC.Tc.Utils.Unify.checkCo. , and is what `cteCoercionHole` reason in + `CheckTyEqResult` means. + + * These special hetero-kind CoercionHoles are created by the `uType` unifier when + the parent's CtOrigin is KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole + and friends. + + We set this origin, via `updUEnvLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`. + + * We /also/ add the coercion hole to the `RewriterSet` of the constraint, + in `canEqCanLHSHetero` + + * When filling one of these special hetero-kind coercion holes, we kick out + any IrredCt's that mention this hole; maybe it is now canonical. + See `kickOutAfterFillingCoercionHole`. - * Hetero-kind CoercionHoles are created when the parent's CtOrigin is - KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole and friends. We - set this origin, via `mkKindLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`. + Gah! This is bizarrely complicated. (EIK3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the algorithm detailed here, producing [W] co :: k1 ~ k2, and adding ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -466,10 +466,13 @@ kickOutAfterUnification tv_list = case nonEmpty tv_list of ; return n_kicked } kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () --- See Wrinkle (EIK2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality +-- See Wrinkle (EIK2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality -- It's possible that this could just go ahead and unify, but could there be occurs-check -- problems? Seems simpler just to kick out. kickOutAfterFillingCoercionHole hole + | not (isHeteroKindCoHole hole) + = return () -- Only hetero-kind coeercion holes provoke kick-out + | otherwise = do { ics <- getInertCans ; let (kicked_out, ics') = kick_out ics n_kicked = lengthBag kicked_out @@ -493,9 +496,9 @@ kickOutAfterFillingCoercionHole hole where (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds - kick_ct :: IrredCt -> Bool - -- True: kick out; False: keep. - kick_ct ct + kick_ct :: IrredCt -> Bool -- True: kick out; False: keep. + kick_ct ct -- See (EIK2) in Note [Equalities with incompatible kinds] + -- for this very specific kick-ot stuff | IrredCt { ir_ev = ev, ir_reason = reason } <- ct , CtWanted (WantedCt { ctev_rewriters = RewriterSet rewriters }) <- ev , NonCanonicalReason ctyeq <- reason ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -241,17 +241,23 @@ instance Outputable DictCt where ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ An EqCt is a canonical equality constraint, one that can live in the inert set, and that can be used to rewrite other constraints. It satisfies these invariants: + * (TyEq:OC) lhs does not occur in rhs (occurs check) Note [EqCt occurs check] + * (TyEq:F) rhs has no foralls (this avoids substituting a forall for the tyvar in other types) + * (TyEq:K) typeKind lhs `tcEqKind` typeKind rhs; Note [Ct kind invariant] + * (TyEq:N) If the equality is representational, rhs is not headed by a saturated application of a newtype TyCon. See GHC.Tc.Solver.Equality Note [No top-level newtypes on RHS of representational equalities]. (Applies only when constructor of newtype is in scope.) + * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we will not form an EqCt (a ~ ty). + * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up a hetero-kinded equality. See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality, wrinkle (EIK2) @@ -534,9 +540,12 @@ cteSolubleOccurs = CTEP (bit 3) -- Occurs-check under a type function, or in -- cteSolubleOccurs must be one bit to the left of cteInsolubleOccurs -- See also Note [Insoluble mis-match] in GHC.Tc.Errors -cteCoercionHole = CTEP (bit 4) -- Coercion hole encountered +cteCoercionHole = CTEP (bit 4) -- Kind-equality coercion hole encountered + -- See (EIK2) in Note [Equalities with incompatible kinds] + cteConcrete = CTEP (bit 5) -- Type variable that can't be made concrete -- e.g. alpha[conc] ~ Maybe beta[tv] + cteSkolemEscape = CTEP (bit 6) -- Skolem escape e.g. alpha[2] ~ b[sk,4] cteProblem :: CheckTyEqProblem -> CheckTyEqResult ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -369,6 +369,7 @@ newCoercionHoleO (KindEqOrigin {}) pty = new_coercion_hole True pty newCoercionHoleO _ pty = new_coercion_hole False pty new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole +-- For the Bool, see (EIK2) in Note [Equalities with incompatible kinds] new_coercion_hole hetero_kind pred_ty = do { co_var <- newEvVar pred_ty ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty) ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -578,13 +578,12 @@ zonkCtEvRewriterSet ev@(CtWanted wtd) = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev) ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') } --- | Check whether any coercion hole in a RewriterSet is still unsolved. --- Does this by recursively looking through filled coercion holes until --- one is found that is not yet filled in, at which point this aborts. +-- | Zonk a rewriter set; if a coercion hole in the set has been filled, +-- find all the free un-filled coercion holes in the coercion that fills it zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet zonkRewriterSet (RewriterSet set) = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set - -- this does not introduce non-determinism, because the only + -- This does not introduce non-determinism, because the only -- monadic action is to read, and the combining function is -- commutative where @@ -592,10 +591,11 @@ zonkRewriterSet (RewriterSet set) go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc check_hole :: CoercionHole -> ZonkM RewriterSet - check_hole hole = do { m_co <- unpackCoercionHole_maybe hole - ; case m_co of - Nothing -> return (unitRewriterSet hole) - Just co -> unUCHM (check_co co) } + check_hole hole + = do { m_co <- unpackCoercionHole_maybe hole + ; case m_co of + Nothing -> return (unitRewriterSet hole) -- Not filled + Just co -> unUCHM (check_co co) } -- Filled: look inside check_ty :: Type -> UnfilledCoercionHoleMonoid check_co :: Coercion -> UnfilledCoercionHoleMonoid View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4d2a3dbc6d00dae8f79676846b2a51f8... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4d2a3dbc6d00dae8f79676846b2a51f8... You're receiving this email because of your account on gitlab.haskell.org.