From e3c59191fbd526a244b5ac71de5d6b6803374aea Mon Sep 17 00:00:00 2001 From: Christiaan Baaij Date: Thu, 18 Nov 2021 13:12:18 +0100 Subject: Ensure new Ct/evidence invariant The `ctev_pred` field of a `CtEvidence` is a just a cache for the type of the evidence. More precisely: * For Givens, `ctev_pred` = `varType ctev_evar` * For Wanteds, `ctev_pred` = `evDestType ctev_dest` This new invariant is needed because evidence can become part of a type, via `Castty ty kco`. --- compiler/GHC/Core/Coercion.hs | 8 +++- compiler/GHC/Tc/Solver/Canonical.hs | 10 ++--- compiler/GHC/Tc/Types/Constraint.hs | 76 +++++++++++++++++++++++++++++++------ compiler/GHC/Tc/Utils/TcMType.hs | 17 ++------- 4 files changed, 80 insertions(+), 31 deletions(-) diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 42266d35da..69ce993d14 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -123,7 +123,9 @@ module GHC.Core.Coercion ( multToCo, hasCoercionHoleTy, hasCoercionHoleCo, - HoleSet, coercionHolesOfType, coercionHolesOfCo + HoleSet, coercionHolesOfType, coercionHolesOfCo, + + setCoHoleType ) where import {-# SOURCE #-} GHC.CoreToIface (toIfaceTyCon, tidyToIfaceTcArgs) @@ -2752,3 +2754,7 @@ coercionHolesOfCo :: Coercion -> UniqSet CoercionHole , tcf_hole = const unitUniqSet , tcf_tycobinder = \ _ _ _ -> () } + +-- | Set the type of a 'CoercionHole' +setCoHoleType :: CoercionHole -> Type -> CoercionHole +setCoHoleType h t = setCoHoleCoVar h (setVarType (coHoleCoVar h) t) diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 0ec6532105..67b49c8777 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -1026,7 +1026,7 @@ canNonDecomposableConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct canNonDecomposableConcretePrim ev ty = do { -- Update the evidence to account for the zonk to `ty`. let ki = typeKind ty - new_ev = ev { ctev_pred = mkTyConApp concretePrimTyCon [ki, ty] } + new_ev = setCtEvPredType ev (mkTyConApp concretePrimTyCon [ki, ty]) new_ct = CSpecialCan { cc_ev = new_ev , cc_special_pred = ConcretePrimPred @@ -3136,11 +3136,11 @@ rewriteEvidence old_ev@(CtDerived {}) (Reduction _co new_pred) -- was produced by rewriting, may contain suspended calls to -- (ctEvExpr c), which fails for Derived constraints. -- (Getting this wrong caused #7384.) - continueWith (old_ev { ctev_pred = new_pred }) + continueWith (setCtEvPredType old_ev new_pred) rewriteEvidence old_ev (Reduction co new_pred) | isTcReflCo co -- See Note [Rewriting with Refl] - = continueWith (old_ev { ctev_pred = new_pred }) + = continueWith (setCtEvPredType old_ev new_pred) rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction co new_pred) = do { new_ev <- newGivenEvVar loc (new_pred, new_tm) @@ -3188,12 +3188,12 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- It's all a form of rewriteEvidence, specialised for equalities rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs) | CtDerived {} <- old_ev -- Don't force the evidence for a Derived - = return (old_ev { ctev_pred = new_pred }) + = return (setCtEvPredType old_ev new_pred) | NotSwapped <- swapped , isTcReflCo lhs_co -- See Note [Rewriting with Refl] , isTcReflCo rhs_co - = return (old_ev { ctev_pred = new_pred }) + = return (setCtEvPredType old_ev new_pred) | CtGiven { ctev_evar = old_evar } <- old_ev = do { let new_tm = evCoercion ( mkTcSymCo lhs_co diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 398234fa5d..ed07cad136 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -62,7 +62,7 @@ module GHC.Tc.Types.Constraint ( CtEvidence(..), TcEvDest(..), mkKindLoc, toKindLoc, mkGivenLoc, isWanted, isGiven, isDerived, - ctEvRole, + ctEvRole, setCtEvPredType, wrapType, @@ -504,10 +504,6 @@ of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for CDictCan, This holds by construction; look at the unique place where CDictCan is built (in GHC.Tc.Solver.Canonical). -In contrast, the type of the evidence *term* (ctev_dest / ctev_evar) in -the evidence may *not* be fully zonked; we are careful not to look at it -during constraint solving. See Note [Evidence field of CtEvidence]. - Note [Ct kind invariant] ~~~~~~~~~~~~~~~~~~~~~~~~ CEqCan requires that the kind of the lhs matches the kind @@ -1648,11 +1644,40 @@ wrapType ty skols givens = mkSpecForAllTys skols $ mkPhiTy givens ty * * ************************************************************************ -Note [Evidence field of CtEvidence] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -During constraint solving we never look at the type of ctev_evar/ctev_dest; -instead we look at the ctev_pred field. The evtm/evar field -may be un-zonked. +Note [CtEvidence invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The `ctev_pred` field of a `CtEvidence` is a just a cache for the type +of the evidence. More precisely: + +More precisely: +* For Givens, `ctev_pred` = `varType ctev_evar` +* For Wanteds, `ctev_pred` = `evDestType ctev_dest` + +where + + evDestType :: TcEvDest -> TcType + evDestType (EvVarDest evVar) = varType evVar + evDestType (HoleDest coercionHole) = varType (coHoleCoVar coercionHole) + +The invariant is maintained by `setCtEvPredType`, the only function that +updates the `ctev_pred` field of a `CtEvidence`. + +Why is the invariant important? Because when the evidence is a coercion, it may +be used in (CastTy ty co); and then we may call `typeKind` on that type (e.g. +in the kind-check of `eqType`); and expect to see a fully zonked kind. +(This came up in test T13333, in the MR that fixed #20641, namely !6942.) + +Historical Note [Evidence field of CtEvidence] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In the past we tried leaving the `ctev_evar`/`ctev_dest` field of a +constraint untouched (and hence un-zonked) on the grounds that it is +never looked at. But in fact it is: the evidence can become part of a +type (via `CastTy ty kco`) and we may later ask the kind of that type +and expect a zonked result. (For example, in the kind-check +of `eqType`.) + +The safest thing is simply to keep `ctev_evar`/`ctev_dest` in sync +with `ctev_pref`, as stated in `Note [CtEvidence invariants]`. Note [Bind new Givens immediately] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1695,13 +1720,13 @@ data TcEvDest data CtEvidence = CtGiven -- Truly given, not depending on subgoals { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] - , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence] + , ctev_evar :: EvVar -- See Note [CtEvidence invariants] , ctev_loc :: CtLoc } | CtWanted -- Wanted goal { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] - , ctev_dest :: TcEvDest + , ctev_dest :: TcEvDest -- See Note [CtEvidence invariants] , ctev_nosh :: ShadowInfo -- See Note [Constraint flavours] , ctev_loc :: CtLoc } @@ -1755,6 +1780,33 @@ ctEvEvId (CtWanted { ctev_dest = HoleDest h }) = coHoleCoVar h ctEvEvId (CtGiven { ctev_evar = ev }) = ev ctEvEvId ctev@(CtDerived {}) = pprPanic "ctEvId:" (ppr ctev) +-- | Set the type of CtEvidence. +-- +-- This function ensures that the invariants on 'CtEvidence' hold, by updating +-- the evidence and the ctev_pred in sync with each other. +-- See Note [CtEvidence invariants] +setCtEvPredType :: CtEvidence -> Type -> CtEvidence +setCtEvPredType old_ctev new_pred = case old_ctev of + CtGiven { ctev_evar = ev, ctev_loc = loc } -> + CtGiven { ctev_pred = new_pred + , ctev_evar = setVarType ev new_pred + , ctev_loc = loc + } + CtWanted { ctev_dest = dest, ctev_nosh = nosh, ctev_loc = loc } -> + CtWanted { ctev_pred = new_pred + , ctev_dest = new_dest + , ctev_nosh = nosh + , ctev_loc = loc + } + where + new_dest = case dest of + EvVarDest ev -> EvVarDest (setVarType ev new_pred) + HoleDest h -> HoleDest (setCoHoleType h new_pred) + CtDerived { ctev_loc = loc } -> + CtDerived { ctev_pred = new_pred + , ctev_loc = loc + } + instance Outputable TcEvDest where ppr (HoleDest h) = text "hole" <> ppr h ppr (EvVarDest ev) = ppr ev diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 9f279a9349..699bf5f69a 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -2407,19 +2407,10 @@ zonkCt ct ; return (mkNonCanonical fl') } zonkCtEvidence :: CtEvidence -> TcM CtEvidence -zonkCtEvidence ctev@(CtGiven { ctev_pred = pred }) - = do { pred' <- zonkTcType pred - ; return (ctev { ctev_pred = pred'}) } -zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest }) - = do { pred' <- zonkTcType pred - ; let dest' = case dest of - EvVarDest ev -> EvVarDest $ setVarType ev pred' - -- necessary in simplifyInfer - HoleDest h -> HoleDest h - ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) } -zonkCtEvidence ctev@(CtDerived { ctev_pred = pred }) - = do { pred' <- zonkTcType pred - ; return (ctev { ctev_pred = pred' }) } +zonkCtEvidence ctev + = do { pred' <- zonkTcType (ctev_pred ctev) + ; return (setCtEvPredType ctev pred') + } zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty -- cgit v1.2.1