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`.

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