[Git][ghc/ghc][wip/amg/dcoercion] WIP: remove LHS type in Reduction

sheaf (@sheaf) gitlab at gitlab.haskell.org
Fri May 12 23:18:08 UTC 2023



sheaf pushed to branch wip/amg/dcoercion at Glasgow Haskell Compiler / GHC


Commits:
5e07c825 by sheaf at 2023-05-13T01:17:50+02:00
WIP: remove LHS type in Reduction

- - - - -


20 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/Opt/WorkWrap/Utils.hs
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/Gen/Foreign.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Types/Id/Make.hs
- testsuite/tests/dcoercion/DCo_Phantom.hs
- testsuite/tests/dcoercion/DCo_Phantom.stderr
- testsuite/tests/dcoercion/DCo_Specialise.hs
- testsuite/tests/dcoercion/DCo_T15703_aux.hs


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1011,6 +1011,8 @@ mkSubDCo l_ty dco r_ty = case dco of
     | Just (tc, arg_l_tys) <- splitTyConApp_maybe l_ty
     , Just (_ , arg_r_tys) <- splitTyConApp_maybe r_ty
     -> TyConAppDCo (applyRoles_dco tc arg_l_tys dcos arg_r_tys)
+    -- SLD TODO: we might need to get rid of this case,
+    -- to avoid calling applyRoles, which calls mkHydrateDCo.
   DehydrateCo co
     -> DehydrateCo (mkSubCo co)
   UnivDCo prov r
@@ -1188,6 +1190,7 @@ See Note [The Reduction type] in GHC.Core.Reduction.
 mkHydrateDCo :: HasDebugCallStack => Role -> Type -> DCoercion -> Maybe Type -> Coercion
 mkHydrateDCo r l_ty dco mb_r_ty
   | debugIsOn
+  , isNothing mb_r_ty
   -- Check that 'followDCo' does not crash,
   -- i.e. that the Hydration invariant is satisfied.
   = check_hydration_invariant r l_ty dco $
@@ -1447,7 +1450,7 @@ expandOneStepDCo check_prop throw_err r l_ty
 
       -- LHS type is not a TyConApp.
       Nothing ->
-        throw_err (text"StepsDCo: LHS not a TyConApp" $$ debug_info)
+        throw_err (text "StepsDCo: LHS not a TyConApp" $$ debug_info)
   where
     debug_info = vcat [ text "r:" <+> ppr r
                       , text "l_ty:" <+> ppr l_ty ]
@@ -1774,9 +1777,11 @@ mkSelCo_maybe cs co
       -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
       -- then (nth SelForAll co :: (t1 ~ t2) ~N (t3 ~ t4))
 
-    go SelForAll (HydrateDCo r _ (ForAllDCo tv kind_co _) _)
-      = assert (r == Nominal) $
-        Just $ mkHydrateDCo Nominal (tyVarKind tv) kind_co Nothing
+    go SelForAll dco@(HydrateDCo _ _ (ForAllDCo tv kind_co _) rhs)
+      = case splitForAllTyCoVar_maybe rhs of
+          Just (tv', _) -> Just $
+            mkHydrateDCo Nominal (tyVarKind tv) kind_co (Just $ tyVarKind tv')
+          _ -> pprPanic "mkSelCo_maybe" (ppr dco $$ ppr rhs)
 
     go (SelFun fs) (FunCo _ _ _ w arg res)
       = Just (getNthFun fs w arg res)
@@ -1820,7 +1825,7 @@ mkSelCo_maybe cs co
     good_call SelForAll
       | Just (_tv1, _) <- splitForAllTyCoVar_maybe ty1
       , Just (_tv2, _) <- splitForAllTyCoVar_maybe ty2
-      =  True
+      = True
 
     good_call (SelFun {})
        = isFunTy ty1 && isFunTy ty2
@@ -2083,6 +2088,7 @@ setNominalRole_maybe_dco r ty (TransDCo dco1 dco2)
   = TransDCo <$> setNominalRole_maybe_dco r ty dco1 <*> setNominalRole_maybe_dco r mid_ty dco2
   where
     mid_ty = followDCo r ty dco1
+      -- OK to call followDCo here: this function is always called on fully zonked types.
 setNominalRole_maybe_dco _ _ (SubDCo dco) = Just dco
 setNominalRole_maybe_dco r _ (DehydrateCo co) = DehydrateCo <$> setNominalRole_maybe r co
 setNominalRole_maybe_dco _ _ (UnivDCo prov rhs)


=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -1350,7 +1350,7 @@ topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction
 -- original type, and the returned coercion is always homogeneous.
 topNormaliseType_maybe env ty
   = do { ((dco, mkind_co), nty) <- topNormaliseTypeX stepper combine ty
-       ; return $ homogeniseRedn (mkReduction ty dco nty) mkind_co }
+       ; return $ homogeniseRedn (mkReduction dco nty) mkind_co }
   where
     stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper
 
@@ -1365,7 +1365,7 @@ topNormaliseType_maybe env ty
     tyFamStepper :: NormaliseStepper (DCoercion, MCoercionN)
     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
       = case topReduceTyFamApp_maybe env tc tys of
-          Just (HetReduction (Reduction _ co rhs) res_co)
+          Just (HetReduction (Reduction co rhs) res_co)
             -> NS_Step rec_nts rhs (co, res_co)
           _ -> NS_Done
 
@@ -1388,7 +1388,7 @@ topReduceTyFamApp_maybe envs fam_tc arg_tys
   = Nothing
   where
     role = Representational
-    ArgsReductions args_redns@(Reductions _ _ ntys) res_co
+    ArgsReductions args_redns@(Reductions _ ntys) res_co
       = initNormM envs role (tyCoVarsOfTypes arg_tys)
       $ normalise_tc_args fam_tc arg_tys
 
@@ -1424,7 +1424,7 @@ normalise_tc_app tc tys
   = -- A type-family application
     do { env <- getEnv
        ; role <- getRole
-       ; ArgsReductions redns@(Reductions _ _ ntys) res_co <- normalise_tc_args tc tys
+       ; ArgsReductions redns@(Reductions _ ntys) res_co <- normalise_tc_args tc tys
        ; case reduceTyFamApp_maybe env role tc ntys of
            Just redn1
              -> do { redn2 <- normalise_reduction redn1
@@ -1441,7 +1441,7 @@ normalise_tc_app tc tys
     do { ArgsReductions redns res_co <- normalise_tc_args tc tys
        ; role <- getRole
        ; return $
-           homogeniseRedn (mkTyConAppRedn_MightBeSynonym role tc redns) res_co }
+           homogeniseRedn (mkTyConAppRedn_MightBeSynonym role tc tys redns) res_co }
              -- NB: we assume "tys" satisfy the hydration invariant from
              -- Note [The Hydration invariant] in GHC.Core.Coercion,
              -- because the "normalise" functions all only deal with fully zonked types.
@@ -1501,7 +1501,7 @@ normalise_type ty
     -- cf. GHC.Tc.Solver.Rewrite.rewrite_app_ty_args
     go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys)
     go_app_tys fun_ty arg_tys
-      = do { fun_redn@(Reduction _ _ nfun) <- go fun_ty
+      = do { fun_redn@(Reduction _ nfun) <- go fun_ty
            ; case tcSplitTyConApp_maybe nfun of
                Just (tc, xis) ->
                  do { redn <- go (mkTyConApp tc (xis ++ arg_tys))
@@ -1532,7 +1532,7 @@ normalise_args :: Kind    -- of the function
 -- cf. GHC.Tc.Solver.Rewrite.rewrite_args_slow
 normalise_args fun_ki roles args
   = do { normed_args <- zipWithM normalise1 (Inf.toList roles) args
-       ; return $ simplifyArgsWorker ki_binders inner_ki fvs roles normed_args }
+       ; return $ simplifyArgsWorker ki_binders inner_ki fvs roles args normed_args }
   where
     (ki_binders, inner_ki) = splitPiTys fun_ki
     fvs = tyCoVarsOfTypes args
@@ -1550,7 +1550,7 @@ normalise_tyvar tv
            Nothing -> mkReflRedn (mkTyVarTy tv) }
 
 normalise_reduction :: Reduction -> NormM Reduction
-normalise_reduction redn@(Reduction _ _ ty)
+normalise_reduction redn@(Reduction _ ty)
   = do { redn' <- normalise_type ty
        ; return $ redn `mkTransRedn` redn' }
 
@@ -1560,10 +1560,11 @@ normalise_var_bndr tcvar
   = do { lc1 <- getLC
        ; env <- getEnv
        ; let
-           do_normalise ki = do { redn <- normalise_type ki; return redn }
-           callback lc ki  = runNormM (do_normalise ki) env lc Nominal
-       ; return $ liftCoSubstVarBndrUsing (mkHydrateReductionDCoercion Nominal)
-                    callback lc1 tcvar }
+           mk_co (lhs, redn)    = mkHydrateReductionDCoercion Nominal lhs redn
+           do_normalise ki      = do { redn <- normalise_type ki; return (ki, redn) }
+           callback lc ki       = runNormM (do_normalise ki) env lc Nominal
+           (lc, tcv, (_, redn)) = liftCoSubstVarBndrUsing mk_co callback lc1 tcvar
+       ; return (lc, tcv, redn) }
 
 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
 -- a 'LiftingContext', and a 'Role'.


=====================================
compiler/GHC/Core/Opt/Simplify/Iteration.hs
=====================================
@@ -3254,9 +3254,11 @@ improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
            -> SimplM (SimplEnv, OutExpr, OutId)
 -- Note [Improving seq]
 improveSeq fam_envs env scrut case_bndr case_bndr1 [Alt DEFAULT _ _]
-  | Just redn@(Reduction _ _ ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1)
+  | let ty1 = idType case_bndr1
+  , Just redn@(Reduction _ ty2) <- topNormaliseType_maybe fam_envs ty1
   = do { case_bndr2 <- newId (fsLit "nt") ManyTy ty2
-        ; let co   = mkHydrateReductionDCoercion Representational redn
+        ; let co   = mkHydrateReductionDCoercion Representational ty1 redn
+                     -- SLD TODO: OK because zonked.
               rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co) Nothing
               env2 = extendIdSubst env case_bndr rhs
         ; return (env2, scrut `Cast` co, case_bndr2) }


=====================================
compiler/GHC/Core/Opt/WorkWrap/Utils.hs
=====================================
@@ -1316,7 +1316,7 @@ findTypeShape fam_envs ty
        = TsUnk
 
     go_tc rec_tc tc tc_args
-       | Just (HetReduction (Reduction _ _ rhs) _) <- topReduceTyFamApp_maybe fam_envs tc tc_args
+       | Just (HetReduction (Reduction _ rhs) _) <- topReduceTyFamApp_maybe fam_envs tc tc_args
        = go rec_tc rhs
 
        | Just con <- tyConSingleAlgDataCon_maybe tc
@@ -1411,7 +1411,7 @@ isRecDataCon fam_envs fuel orig_dc
     go_tc_app fuel visited_tcs tc tc_args =
       case tyConDataCons_maybe tc of
       --- | pprTrace "tc_app" (vcat [ppr tc, ppr tc_args]) False = undefined
-        _ | Just (HetReduction (Reduction _ _ rhs) _) <- topReduceTyFamApp_maybe fam_envs tc tc_args
+        _ | Just (HetReduction (Reduction _ rhs) _) <- topReduceTyFamApp_maybe fam_envs tc tc_args
           -- This is the only place where we look at tc_args, which might have
           -- See Note [Detecting recursive data constructors], point (C) and (5)
           -> go_arg_ty fuel visited_tcs rhs


=====================================
compiler/GHC/Core/Reduction.hs
=====================================
@@ -62,27 +62,23 @@ Note [The Reduction type]
 Many functions in the type-checker rewrite a type, using Given type equalities
 or type-family reductions, and return a Reduction:
 
-  data Reduction = Reduction Type Coercion !Type
+  data Reduction = Reduction Coercion !Type
 
-When we rewrite ty at role r, producing Reduction ty' dco xi, we guarantee:
+When we rewrite ty at role r, producing Reduction dco xi, we guarantee:
 
-  RW1: ty' is equal to ty (up to zonking)
-  RW2: followDCo r ty' dco is equal to xi (up to zonking)
+  RW2: followDCo r (zonk ty) dco is equal to xi, up to zonking
 
-In particular, this means that `dco :: ty' ~r xi`. Note that we need to use ty',
-and not ty, to satisfy RW2; see Note [The Hydration invariant] in GHC.Core.Coercion.
-It could be the case that `followDCo r ty dco` crashes, e.g. if `ty` is a metavariable
-and `dco = TyConAppDCo ..`. This is why we store the LHS type in the Reduction too.
+In particular, this means that `dco :: ty ~r xi`. Note however that we might
+need to zonk... SLD TODO explain.
 
 The order of the arguments to the constructor serves as a reminder
-of what the Type is.  In
+of what the Type is. In
 
-    Reduction ty' dco xi
+    ty ~rewrites to~> Reduction dco xi
 
-the original type ty appears to the left, and the result appears on the right,
-reminding us that we must have:
+the result appears on the right, reminding us that we must have:
 
-  dco :: ty' ~r xi
+  dco :: ty ~r xi
 
 Example functions that use this datatype:
 
@@ -104,21 +100,16 @@ a tuple (with all fields lazy), gives several advantages (see #20161)
 -- | A 'Reduction' is the result of an operation that rewrites a type @ty_in at .
 -- The 'Reduction' includes:
 --
---  - an input type @ty_in'@, equal to @ty_in@ up to zonking,
 --  - a directed coercion @dco@,
 --  - the rewritten type @ty_out@
 --
--- such that @dco :: ty_in' ~ ty_out@, where the role @r@ of the coercion is determined
--- by the context.
---
--- Invariant: it is always valid to call @followDCo r ty_in' dco@, as per
--- Note [The Hydration invariant] in GHC.Core.Coercion.
+-- such that @dco :: ty_in ~ ty_out@, where the role @r@ of the coercion
+-- is determined by the context.
 --
 -- See Note [The Reduction type].
 data Reduction =
   Reduction
-    { reductionOriginalType :: Type
-    , reductionDCoercion    :: DCoercion
+    { reductionDCoercion    :: DCoercion
     , reductionReducedType  :: !Type
     }
 -- N.B. the 'Coercion' field must be lazy: see for instance GHC.Tc.Solver.Rewrite.rewrite_tyvar2
@@ -134,12 +125,9 @@ type ReductionR = Reduction
 
 -- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.
 --
--- Pre-condition: the RHS type of the coercion matches the provided type
--- (perhaps up to zonking).
---
 -- Use 'coercionRedn' when you only have the coercion.
-mkReduction :: Type -> DCoercion -> Type -> Reduction
-mkReduction lty co rty = Reduction lty co rty
+mkReduction :: DCoercion -> Type -> Reduction
+mkReduction co rty = Reduction co rty
 {-# INLINE mkReduction #-}
 
 instance Outputable Reduction where
@@ -149,18 +137,17 @@ instance Outputable Reduction where
       , text "   reductionDCoercion:" <+> ppr (reductionDCoercion redn)
       ]
 
--- | Turn a 'Coercion' into a 'Reduction'
--- by inspecting the LHS and RHS types of the coercion, and dehydrating.
+-- | Turn a 'Coercion' into a 'Reduction' by dehydrating.
 --
 -- Prefer using 'mkReduction' wherever possible to avoid doing these indirections.
 mkDehydrateCoercionRedn :: Coercion -> Reduction
 mkDehydrateCoercionRedn co =
-  Reduction (coercionLKind co) (mkDehydrateCo co) (coercionRKind co)
+  Reduction (mkDehydrateCo co) (coercionRKind co)
 {-# INLINE mkDehydrateCoercionRedn #-}
 
 -- | Hydrate the 'DCoercion' stored inside a 'Reduction' into a full-fledged 'Coercion'.
-mkHydrateReductionDCoercion :: HasDebugCallStack => Role -> Reduction -> Coercion
-mkHydrateReductionDCoercion r (Reduction lty dco rty) = mkHydrateDCo r lty dco (Just rty)
+mkHydrateReductionDCoercion :: HasDebugCallStack => Role -> Type -> Reduction -> Coercion
+mkHydrateReductionDCoercion r lty (Reduction dco rty) = mkHydrateDCo r lty dco (Just rty)
   -- N.B.: we use the LHS type stored in the 'Reduction' to ensure
   -- we satisfy the Hydration invariant of Note [The Hydration invariant]
   -- in GHC.Core.Coercion.
@@ -168,8 +155,8 @@ mkHydrateReductionDCoercion r (Reduction lty dco rty) = mkHydrateDCo r lty dco (
 
 -- | Downgrade the role of the directed coercion stored in the 'Reduction',
 -- from 'Nominal' to 'Representational'.
-mkSubRedn :: Reduction -> Reduction
-mkSubRedn redn@(Reduction lhs dco rhs)
+mkSubRedn :: HasDebugCallStack => Type -> Reduction -> Reduction
+mkSubRedn lhs redn@(Reduction dco rhs)
   = redn { reductionDCoercion = mkSubDCo lhs dco rhs }
 {-# INLINE mkSubRedn #-}
 
@@ -183,13 +170,13 @@ mkSubRedn redn@(Reduction lhs dco rhs)
 -- as required by Note [The Reduction type]. You must manually ensure this
 -- invariant.
 mkTransRedn :: Reduction -> Reduction -> Reduction
-mkTransRedn (Reduction ty1 dco1 _) (Reduction _ dco2 ty2)
-  = Reduction ty1 (dco1 `mkTransDCo` dco2) ty2
+mkTransRedn (Reduction dco1 _) (Reduction dco2 ty2)
+  = Reduction (dco1 `mkTransDCo` dco2) ty2
 {-# INLINE mkTransRedn #-}
 
 -- | The reflexive reduction.
 mkReflRedn :: Type -> Reduction
-mkReflRedn ty = mkReduction ty mkReflDCo ty
+mkReflRedn ty = mkReduction mkReflDCo ty
 {-# INLINE mkReflRedn #-}
 
 -- | Create a 'Reduction' from a kind cast, in which
@@ -201,7 +188,6 @@ mkReflRedn ty = mkReduction ty mkReflDCo ty
 mkGReflRightRedn :: Type -> CoercionN -> Reduction
 mkGReflRightRedn ty co
   = mkReduction
-      ty
       (mkGReflRightDCo co)
       (mkCastTy ty co)
 {-# INLINE mkGReflRightRedn #-}
@@ -217,7 +203,6 @@ mkGReflRightMRedn ty MRefl
   = mkReflRedn ty
 mkGReflRightMRedn ty (MCo kco)
   = mkReduction
-      ty
       (mkGReflRightDCo kco)
       (mkCastTy ty kco)
 {-# INLINE mkGReflRightMRedn #-}
@@ -231,7 +216,6 @@ mkGReflRightMRedn ty (MCo kco)
 mkGReflLeftRedn :: Type -> CoercionN -> Reduction
 mkGReflLeftRedn ty co
   = mkReduction
-      (mkCastTy ty co)
       (mkGReflLeftDCo co)
       ty
 {-# INLINE mkGReflLeftRedn #-}
@@ -247,7 +231,6 @@ mkGReflLeftMRedn ty MRefl
   = mkReflRedn ty
 mkGReflLeftMRedn ty (MCo kco)
   = mkReduction
-      (mkCastTy ty kco)
       (mkGReflLeftDCo kco)
       ty
 {-# INLINE mkGReflLeftMRedn #-}
@@ -259,9 +242,8 @@ mkGReflLeftMRedn ty (MCo kco)
 -- of the given 'Role' (which must match the role of the coercion stored
 -- in the 'Reduction' argument).
 mkCoherenceRightRedn :: Reduction -> CoercionN -> Reduction
-mkCoherenceRightRedn (Reduction ty1 co1 ty2) kco
+mkCoherenceRightRedn (Reduction co1 ty2) kco
   = mkReduction
-      ty1
       (mkCoherenceRightDCo kco co1)
       (mkCastTy ty2 kco)
 {-# INLINE mkCoherenceRightRedn #-}
@@ -274,9 +256,8 @@ mkCoherenceRightRedn (Reduction ty1 co1 ty2) kco
 -- in the 'Reduction' argument).
 mkCoherenceRightMRedn :: Reduction -> MCoercionN -> Reduction
 mkCoherenceRightMRedn redn MRefl = redn
-mkCoherenceRightMRedn (Reduction ty1 co1 ty2) (MCo kco)
+mkCoherenceRightMRedn (Reduction co1 ty2) (MCo kco)
   = mkReduction
-      ty1
       (mkCoherenceRightDCo kco co1)
       (mkCastTy ty2 kco)
 {-# INLINE mkCoherenceRightMRedn #-}
@@ -293,11 +274,10 @@ mkCoherenceRightMRedn (Reduction ty1 co1 ty2) (MCo kco)
 mkCastRedn1 :: CoercionN -- ^ coercion to cast with
             -> Reduction  -- ^ rewritten type, with rewriting coercion
             -> Reduction
-mkCastRedn1 cast_co (Reduction ty dco xi)
+mkCastRedn1 cast_co (Reduction dco xi)
   -- co :: ty ~r ty'
   -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)
   = mkReduction
-      (mkCastTy ty cast_co)
       (castDCoercionKind1 dco cast_co)
       (mkCastTy xi cast_co)
 {-# INLINE mkCastRedn1 #-}
@@ -313,9 +293,8 @@ mkCastRedn2 :: CoercionN -- ^ coercion to cast with on the left
             -> Reduction -- ^ rewritten type, with rewriting coercion
             -> CoercionN -- ^ coercion to cast with on the right
             -> Reduction
-mkCastRedn2 cast_co (Reduction ty nco nty) cast_co'
+mkCastRedn2 cast_co (Reduction nco nty) cast_co'
   = mkReduction
-      (mkCastTy ty cast_co)
       (castDCoercionKind2 nco cast_co cast_co')
       (mkCastTy nty cast_co')
 {-# INLINE mkCastRedn2 #-}
@@ -324,9 +303,8 @@ mkCastRedn2 cast_co (Reduction ty nco nty) cast_co'
 --
 -- Combines 'mkAppCo' and 'mkAppTy`.
 mkAppRedn :: Reduction -> Reduction -> Reduction
-mkAppRedn (Reduction lty1 co1 rty1) (Reduction lty2 co2 rty2)
+mkAppRedn (Reduction co1 rty1) (Reduction co2 rty2)
   = mkReduction
-      (mkAppTy lty1 lty2)
       (mkAppDCo co1 co2)
       (mkAppTy rty1 rty2)
 {-# INLINE mkAppRedn #-}
@@ -342,13 +320,12 @@ mkFunRedn :: FunTyFlag
           -> Reduction  -- ^ result reduction
           -> Reduction
 mkFunRedn af
-  (Reduction w_lty w_co w_rty)
+  (Reduction w_co w_rty)
   arg_repco
   res_repco
-  (Reduction arg_lty arg_co arg_rty)
-  (Reduction res_lty res_co res_rty)
+  (Reduction arg_co arg_rty)
+  (Reduction res_co res_rty)
     = mkReduction
-        (mkFunTy af w_lty arg_lty res_lty)
         (mkFunDCo w_co arg_repco res_repco arg_co res_co)
         (mkFunTy af w_rty arg_rty res_rty)
 {-# INLINE mkFunRedn #-}
@@ -362,9 +339,8 @@ mkForAllRedn :: ForAllTyFlag
              -> ReductionN -- ^ kind reduction
              -> Reduction  -- ^ body reduction
              -> Reduction
-mkForAllRedn vis tv1 (Reduction _ h rki) (Reduction lty co rty)
+mkForAllRedn vis tv1 (Reduction h rki) (Reduction co rty)
   = mkReduction
-      (mkForAllTy (Bndr tv1 vis) lty)
       (mkForAllDCo tv1 h co)
       (mkForAllTy (Bndr tv2 vis) rty)
   where
@@ -376,9 +352,8 @@ mkForAllRedn vis tv1 (Reduction _ h rki) (Reduction lty co rty)
 --
 -- Combines 'mkHomoForAllCos' and 'mkForAllTys'.
 mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
-mkHomoForAllRedn bndrs (Reduction ty1 co ty2)
+mkHomoForAllRedn bndrs (Reduction co ty2)
   = mkReduction
-      (mkForAllTys bndrs ty1)
       (mkHomoForAllDCos (binderVars bndrs) co)
       (mkForAllTys bndrs ty2)
 {-# INLINE mkHomoForAllRedn #-}
@@ -390,22 +365,18 @@ mkProofIrrelRedn :: Coercion   -- ^ lhs_co
                  -> DCoercionN -- ^ dco :: lhs_co ~ rhs_co
                  -> Coercion   -- ^ rhs_co
                  -> Reduction
-mkProofIrrelRedn g1 co g2
+mkProofIrrelRedn _g1 co g2
   = mkReduction
-      lhs_co
       (mkProofIrrelDCo co rhs_co)
       rhs_co
   where
-    lhs_co = mkCoercionTy g1
     rhs_co = mkCoercionTy g2
 {-# INLINE mkProofIrrelRedn #-}
 
 -- | Create a reflexive 'Reduction' whose LHS and RHS is the given 'Coercion',
 -- with the specified 'Role'.
 mkReflCoRedn :: Coercion -> Reduction
-mkReflCoRedn co = mkReduction co_ty mkReflDCo co_ty
-  where
-    co_ty = mkCoercionTy co
+mkReflCoRedn co = mkReduction mkReflDCo (mkCoercionTy co)
 {-# INLINE mkReflCoRedn #-}
 
 -- | A collection of 'Reduction's where the coercions and the types are stored separately.
@@ -417,22 +388,22 @@ mkReflCoRedn co = mkReduction co_ty mkReflDCo co_ty
 --
 -- Invariant: given @Reductions lhs_tys dcos rhs_tys@, and an ambient role @r@,
 -- we can obtain the @rhs_tys@ by following the directed coercions starting from the repsective
--- @lhs_tys at . Equivalent, @zipWith (followDCo r) lhs_tys dcos@ is equal (up to zonking) to @rhs_tys at .
-data Reductions = Reductions [Type] [DCoercion] [Type]
+-- @lhs_tys at . Equivalently, @zipWith (followDCo r) lhs_tys dcos@ is equal (up to zonking) to @rhs_tys at .
+data Reductions = Reductions [DCoercion] [Type]
 
 instance Outputable Reductions where
-  ppr (Reductions ltys dcos rtys) = parens (text "Reductions" <+> ppr ltys <+> ppr dcos <+> ppr rtys)
+  ppr (Reductions dcos rtys) = parens (text "Reductions" <+> ppr dcos <+> ppr rtys)
 
 -- | Create 'Reductions' from individual lists of coercions and types.
 --
 -- The lists should be of the same length, and the RHS type of each coercion
 -- should match the specified type in the other list.
-mkReductions :: [Type] -> [DCoercion] -> [Type] -> Reductions
-mkReductions tys1 cos tys2 = Reductions tys1 cos tys2
+mkReductions :: [DCoercion] -> [Type] -> Reductions
+mkReductions cos tys2 = Reductions cos tys2
 {-# INLINE mkReductions #-}
 
 mkReflRedns :: [Type] -> Reductions
-mkReflRedns tys = mkReductions tys (mkReflDCos tys) tys
+mkReflRedns tys = mkReductions (mkReflDCos tys) tys
 {-# INLINE mkReflRedns #-}
 
 mkReflDCos :: [Type] -> [DCoercion]
@@ -441,8 +412,8 @@ mkReflDCos tys = replicate (length tys) mkReflDCo
 
 -- | Combines 'mkAppCos' and 'mkAppTys'.
 mkAppRedns :: Reduction -> Reductions -> Reduction
-mkAppRedns (Reduction ty1 co ty2) (Reductions tys1 cos tys2)
-  = mkReduction (mkAppTys ty1 tys1) (mkAppDCos co cos) (mkAppTys ty2 tys2)
+mkAppRedns (Reduction co ty2) (Reductions cos tys2)
+  = mkReduction (mkAppDCos co cos) (mkAppTys ty2 tys2)
 {-# INLINE mkAppRedns #-}
 
 -- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
@@ -450,15 +421,15 @@ mkAppRedns (Reduction ty1 co ty2) (Reductions tys1 cos tys2)
 -- Use this when you know the 'TyCon' is not a type synonym. If it might be,
 -- use 'mkTyConAppRedn_MightBeSynonym'.
 mkTyConAppRedn :: TyCon -> Reductions -> Reduction
-mkTyConAppRedn tc (Reductions tys1 cos tys2)
-  = mkReduction (mkTyConApp tc tys1) (mkTyConAppDCo cos) (mkTyConApp tc tys2)
+mkTyConAppRedn tc (Reductions cos tys2)
+  = mkReduction (mkTyConAppDCo cos) (mkTyConApp tc tys2)
 {-# INLINE mkTyConAppRedn #-}
 
 -- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
 --
 -- Use 'mkTyConAppRedn' if the 'TyCon' is definitely not a type synonym.
-mkTyConAppRedn_MightBeSynonym :: Role -> TyCon -> Reductions -> Reduction
-mkTyConAppRedn_MightBeSynonym role tc redns@(Reductions tys1 dcos tys2)
+mkTyConAppRedn_MightBeSynonym :: Role -> TyCon -> [Type] -> Reductions -> Reduction
+mkTyConAppRedn_MightBeSynonym role tc tys1 redns@(Reductions dcos tys2)
   -- 'mkTyConAppCo' handles synomyms by using substitution lifting.
   -- We don't have that for directed coercions, so we use hydrate/dehydrate
   -- so that we can call 'liftCoSubst'.
@@ -466,8 +437,8 @@ mkTyConAppRedn_MightBeSynonym role tc redns@(Reductions tys1 dcos tys2)
   -- for directed coercions to avoid this (and a similar issue in simplifyArgsWorker).
   | ExpandsSyn tv_dco_prs rhs_ty leftover_dcos <- expandSynTyCon_maybe tc dcos
   , let tv_co_prs = zipWith4 hydrate (tyConRoleListX role tc) tys1 tv_dco_prs tys2
-  = mkReduction
-      (mkTyConApp tc tys1)
+  = -- SLD TODO: assert this is a non-forgetful TySyn with no TyFams on the RHS
+    mkReduction
       (mkAppDCos (mkDehydrateCo $ liftCoSubst role (mkLiftingContext tv_co_prs) rhs_ty) leftover_dcos)
       (mkTyConApp tc tys2)
   | otherwise = mkTyConAppRedn tc redns
@@ -477,25 +448,25 @@ mkTyConAppRedn_MightBeSynonym role tc redns@(Reductions tys1 dcos tys2)
     -- which are stored in 'Reductions'.
     -- This upholds the necessary hydration invariant from
     -- Note [The Hydration invariant] in GHC.Core.Coercion.
+    -- SLD TODO...
     {-# INLINE hydrate #-}
 {-# INLINE mkTyConAppRedn_MightBeSynonym #-}
 
 -- | Reduce the arguments of a 'Class' 'TyCon'.
 mkClassPredRedn :: Class -> Reductions -> Reduction
-mkClassPredRedn cls (Reductions tys1 cos tys2)
+mkClassPredRedn cls (Reductions cos tys2)
   = mkReduction
-      (mkClassPred cls tys1)
       (mkTyConAppDCo cos)
       (mkClassPred cls tys2)
 {-# INLINE mkClassPredRedn #-}
 
 -- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.
 unzipRedns :: [Reduction] -> Reductions
-unzipRedns = foldr accRedn (Reductions [] [] [])
+unzipRedns = foldr accRedn (Reductions [] [])
   where
     accRedn :: Reduction -> Reductions -> Reductions
-    accRedn (Reduction ty co xi) (Reductions tys cos xis)
-      = Reductions (ty:tys) (co:cos) (xi:xis)
+    accRedn (Reduction co xi) (Reductions cos xis)
+      = Reductions (co:cos) (xi:xis)
 {-# INLINE unzipRedns #-}
 -- NB: this function is currently used in two locations:
 --
@@ -887,6 +858,7 @@ simplifyArgsWorker :: HasDebugCallStack
                        -- list of binders can be shorter or longer than the list of args
                    -> TyCoVarSet   -- free vars of the args
                    -> Infinite Role-- list of roles, r
+                   -> [Type]       -- original type arguments ty_i
                    -> [Reduction]  -- rewritten type arguments, arg_i
                                    -- each comes with the coercion used to rewrite it,
                                    -- arg_co_i :: ty_i ~ arg_i
@@ -900,10 +872,10 @@ simplifyArgsWorker :: HasDebugCallStack
 -- function is all about. That is, (f xi_1 ... xi_n), where xi_i are the returned arguments,
 -- *is* well kinded.
 simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
-                   orig_roles redns
+                   orig_roles tys redns
   = go orig_lc
        orig_ki_binders orig_inner_ki
-       orig_roles redns
+       orig_roles (zip tys redns)
   where
     orig_lc = emptyLiftingContext $ mkInScopeSet orig_fvs
 
@@ -911,20 +883,20 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
        -> [PiTyBinder]    -- Unsubsted binders of function's kind
        -> Kind            -- Unsubsted result kind of function (not a Pi-type)
        -> Infinite Role   -- Roles at which to rewrite these ...
-       -> [Reduction]     -- rewritten arguments, with their rewriting coercions
+       -> [(Type, Reduction)]   -- rewritten arguments, with their rewriting coercions
        -> ArgsReductions
     go !lc binders inner_ki _ []
         -- The !lc makes the function strict in the lifting context
         -- which means GHC can unbox that pair.  A modest win.
       = ArgsReductions
-          (mkReductions [] [] [])
+          (mkReductions [] [])
           kind_co
       where
         final_kind = mkPiTys binders inner_ki
         kind_co | noFreeVarsOfType final_kind = MRefl
                 | otherwise                   = MCo $ liftCoSubst Nominal lc final_kind
 
-    go lc (binder:binders) inner_ki (Inf role roles) (arg_redn:arg_redns)
+    go lc (binder:binders) inner_ki (Inf role roles) ((orig_ty,arg_redn):arg_redns)
       =  -- We rewrite an argument ty with arg_redn = Reduction arg_co arg
          -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite invariant (F2),
          -- typeKind(ty) = typeKind(arg).
@@ -936,12 +908,13 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
          -- The bangs here have been observed to improve performance
          -- significantly in optimized builds; see #18502
          let !kind_co = liftCoSubst Nominal lc (piTyBinderType binder)
-             !(Reduction arg_ty casted_co casted_xi)
+             !(Reduction casted_co casted_xi)
                       = mkCoherenceRightRedn arg_redn kind_co
          -- now, extend the lifting context with the new binding
              !new_lc | Just tv <- namedPiTyBinder_maybe binder
                      = extendLiftingContextAndInScope lc tv
-                       (mkHydrateDCo role arg_ty casted_co (Just casted_xi))
+                       (mkHydrateDCo role orig_ty casted_co (Just casted_xi))
+                     -- SLD TODO: reword the following.
                      -- NB: this is the crucial place where we need the hydration invariant,
                      -- which is satisfied here as we use the LHS type stored in a 'Reduction'.
                      -- See Note [The Reduction type], as well as
@@ -951,18 +924,19 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
                      -- we need this.
                      | otherwise
                      = lc
-             !(ArgsReductions (Reductions arg_tys cos xis) final_kind_co)
+             !(ArgsReductions (Reductions cos xis) final_kind_co)
                = go new_lc binders inner_ki roles arg_redns
          in ArgsReductions
-              (Reductions (arg_ty:arg_tys) (casted_co:cos) (casted_xi:xis))
+              (Reductions (casted_co:cos) (casted_xi:xis))
               final_kind_co
 
     -- See Note [Last case in simplifyArgsWorker]
-    go lc [] inner_ki roles arg_redns
+    go lc [] inner_ki roles arg_tys_and_redns
       = let co1 = liftCoSubst Nominal lc inner_ki
+            (orig_tys, arg_redns) = unzip arg_tys_and_redns
             co1_kind              = coercionKind co1
-            (arg_cos, res_co)     = decomposePiCos co1 co1_kind (map reductionOriginalType arg_redns)
-            casted_args           = assertPpr (equalLength arg_redns arg_cos)
+            (arg_cos, res_co)     = decomposePiCos co1 co1_kind orig_tys
+            casted_redns          = assertPpr (equalLength arg_redns arg_cos)
                                               (ppr arg_redns $$ ppr arg_cos)
                                   $ zipWith mkCoherenceRightRedn arg_redns arg_cos
                -- In general decomposePiCos can return fewer cos than tys,
@@ -976,6 +950,6 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
             (bndrs, new_inner)    = splitPiTys rewritten_kind
 
             ArgsReductions redns_out res_co_out
-              = go zapped_lc bndrs new_inner roles casted_args
+              = go zapped_lc bndrs new_inner roles (zip orig_tys casted_redns)
         in
           ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out)


=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -68,9 +68,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
    , mkAppDCo, mkForAllDCo, mkReflDCo, mkTransDCo
    , mkGReflRightDCo, mkGReflLeftDCo
    , mkHydrateDCo, mkDehydrateCo, mkUnivDCo
-   , followDCo
    , coercionKind, coercionLKind, coVarKindsTypesRole)
-import GHC.Core.Coercion.Axiom (Role(..))
 import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar )
 import {-# SOURCE #-} GHC.Core.Ppr ( )
 import {-# SOURCE #-} GHC.Core ( CoreExpr )
@@ -1034,8 +1032,8 @@ substForAllCoTyVarBndrUsing co_or_dco sym sty sco (Subst in_scope idenv tenv cen
       DCo -> noFreeVarsOfDCo old_kind_co
     mk_cast = case co_or_dco of
       Co  -> CastTy
-      DCo -> \ ty dco -> CastTy ty (mkHydrateDCo Nominal new_ki1 dco Nothing)
-            -- SLD TODO: Hydration invariant?
+      DCo -> pprPanic "substForAllCoTyVarBndrUsing DCo Sym"
+              (vcat [ text "kind_co:" <+> ppr old_kind_co ])
 
     no_change = no_kind_change && (new_var == old_var)
 
@@ -1060,7 +1058,7 @@ substForAllCoCoVarBndrUsing :: CoOrDCo kco
                             -> (Subst, CoVar, kco)
 substForAllCoCoVarBndrUsing co_or_dco sym sty sco (Subst in_scope idenv tenv cenv)
                             old_var old_kind_co
-  = assert (isCoVar old_var )
+  = assert (isCoVar old_var)
     ( Subst (in_scope `extendInScopeSet` new_var) idenv tenv new_cenv
     , new_var, new_kind_co )
   where
@@ -1079,8 +1077,8 @@ substForAllCoCoVarBndrUsing co_or_dco sym sty sco (Subst in_scope idenv tenv cen
       Co  -> coercionKind new_kind_co
       DCo ->
         let l_ty = sty (varType old_var)
-            r_ty = followDCo Nominal l_ty new_kind_co
-              -- SLD TODO: Hydration invariant satisfied?
+            r_ty = pprPanic "substForAllCoCoVarBndrUsing DCo Sym"
+                   (vcat [ text "kind_co:" <+> ppr old_kind_co])
         in Pair l_ty r_ty
 
     new_var       = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type


=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -2384,10 +2384,10 @@ isEmptyTy ty
 -- coercions via 'topNormaliseType_maybe'. Hence the \"norm\" prefix.
 normSplitTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, [Type], Coercion)
 normSplitTyConApp_maybe fam_envs ty
-  | let Reduction ty' co ty1 = topNormaliseType_maybe fam_envs ty
+  | let Reduction co ty1 = topNormaliseType_maybe fam_envs ty
                                `orElse` (mkReflRedn ty)
   , Just (tc, tc_args) <- splitTyConApp_maybe ty1
-  = Just (tc, tc_args, mkHydrateDCo Representational ty' co (Just ty1))
+  = Just (tc, tc_args, mkHydrateDCo Representational ty co (Just ty1))
     -- N.B.: the hydration invariant is satisfied here, as we have already zonked
     -- everything by the time we call this function.
     -- See Note [The Hydration invariant] in GHC.Core.Coercion.


=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -386,7 +386,7 @@ pmTopNormaliseType (TySt _ inert) typ = {-# SCC "pmTopNormaliseType" #-} do
     tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
     tyFamStepper env rec_nts tc tys  -- Try to step a type/data family
       = case topReduceTyFamApp_maybe env tc tys of
-          Just (HetReduction (Reduction _ _ rhs) _)
+          Just (HetReduction (Reduction _ rhs) _)
             -> NS_Step rec_nts rhs ((rhs:), id)
           _ -> NS_Done
 


=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1494,6 +1494,8 @@ tcIfaceCo = go
     go (IfaceHydrateDCo r t1 dco)= do { t1 <- tcIfaceType t1
                                       ; dco <- tcIfaceDCo dco
                                       ; return $ HydrateDCo r t1 dco (followDCo r t1 dco) }
+                                       -- SLD TODO: investigate perf impact here...
+                                       -- might be worth storing RHS in the interface file...
     go (IfaceUnivCo p r t1 t2)   = UnivCo <$> tcIfaceUnivCoProv go p <*> pure r
                                           <*> tcIfaceType t1 <*> tcIfaceType t2
     go (IfaceSymCo c)            = SymCo    <$> go c


=====================================
compiler/GHC/Tc/Gen/Foreign.hs
=====================================
@@ -171,8 +171,8 @@ normaliseFfiType' env ty0 = runWriterT $ go Representational initRecTc ty0
                       ; return $ mkDehydrateCoercionRedn nt_co `mkTransRedn` redn } } -- AMG TODO
 
         | isFamilyTyCon tc              -- Expand open tycons
-        , redn0@(Reduction l_ty dco ty) <- normaliseTcApp env role tc tys
-        , not (isReflexiveDCo role l_ty dco ty)
+        , redn0@(Reduction dco ty) <- normaliseTcApp env role tc tys
+        , not (isReflexiveDCo role (mkTyConApp tc tys) dco ty)
         = do redn <- go role rec_nts ty
              return $ redn0 `mkTransRedn` redn
 
@@ -252,7 +252,7 @@ tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty
                                     , fd_fi = imp_decl }))
   = setSrcSpanA dloc $ addErrCtxt (foreignDeclCtxt fo)  $
     do { sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
-       ; (redn@(Reduction sig_ty _ norm_sig_ty), gres) <- normaliseFfiType sig_ty
+       ; (redn@(Reduction _ norm_sig_ty), gres) <- normaliseFfiType sig_ty
        ; let
              -- Drop the foralls before inspecting the
              -- structure of the foreign type.
@@ -272,7 +272,7 @@ tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty
        ; imp_decl' <- tcCheckFIType arg_tys res_ty imp_decl
           -- Can't use sig_ty here because sig_ty :: Type and
           -- we need HsType Id hence the undefined
-       ; let co = mkSymCo $ mkHydrateReductionDCoercion Representational redn
+       ; let co = mkSymCo $ mkHydrateReductionDCoercion Representational sig_ty redn
              fi_decl =
                ForeignImport { fd_name = L nloc id
                              , fd_sig_ty = undefined
@@ -413,7 +413,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe
     sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
     rhs <- tcCheckPolyExpr (nlHsVar nm) sig_ty
 
-    (redn@(Reduction sig_ty _ norm_sig_ty), gres) <- normaliseFfiType sig_ty
+    (redn@(Reduction _ norm_sig_ty), gres) <- normaliseFfiType sig_ty
 
     spec' <- tcCheckFEType norm_sig_ty spec
 
@@ -430,7 +430,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe
     return ( mkVarBind id rhs
            , ForeignExport { fd_name = L loc id
                            , fd_sig_ty = undefined
-                           , fd_e_ext = mkHydrateReductionDCoercion Representational redn
+                           , fd_e_ext = mkHydrateReductionDCoercion Representational sig_ty redn
                            , fd_fe = spec' }
            , gres)
 tcFExport d = pprPanic "tcFExport" (ppr d)


=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -210,8 +210,8 @@ canClass :: CtEvidence
 canClass ev cls tys pend_sc
   = -- all classes do *nominal* matching
     assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
-    do { (redns@(Reductions _ _ xis), rewriters) <- rewriteArgsNom ev cls_tc tys
-       ; let redn@(Reduction _ _ xi) = mkClassPredRedn cls redns
+    do { (redns@(Reductions _ xis), rewriters) <- rewriteArgsNom ev cls_tc tys
+       ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns
              mk_ct new_ev = CDictCan { cc_ev = new_ev
                                      , cc_tyargs = xis
                                      , cc_class = cls
@@ -1017,19 +1017,17 @@ the rewriter set. We check this with an assertion.
  -}
 
 
-rewriteEvidence rewriters old_ev (Reduction _ dco new_pred)
+rewriteEvidence rewriters old_ev (Reduction dco new_pred)
   | isReflDCo dco -- See Note [Rewriting with Refl]
   = assert (isEmptyRewriterSet rewriters) $
     continueWith (setCtEvPredType old_ev new_pred)
 
-rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction old_pred dco new_pred)
+rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction dco new_pred)
   = assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted
     do { let
+          old_pred = ctEvPred ev
           dco' = downgradeDCoToRepresentational (ctEvRole ev) old_pred dco new_pred
           co = mkHydrateDCo Representational old_pred dco' (Just new_pred)
-          -- NB: this call to mkHydrateDCo is OK, because of the invariant
-          -- on the LHS type stored in a Reduction. See Note [The Reduction type]
-          -- in GHC.Core.Reduction.
 
           -- mkEvCast optimises ReflCo
           new_tm = mkEvCast (evId old_evar) co
@@ -1040,9 +1038,10 @@ rewriteEvidence new_rewriters
                 ev@(CtWanted { ctev_dest = dest
                              , ctev_loc = loc
                              , ctev_rewriters = rewriters })
-                (Reduction old_pred dco new_pred)
+                (Reduction dco new_pred)
   = do { mb_new_ev <- newWanted loc rewriters' new_pred
        ; let
+          old_pred = ctEvPred ev
           dco' = downgradeDCoToRepresentational (ctEvRole ev) old_pred dco new_pred
           co   = mkHydrateDCo Representational old_pred dco' (Just new_pred)
           -- NB: this call to mkHydrateDCo is OK, because of the invariant


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -237,9 +237,10 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
 -- No similarity in type structure detected. Rewrite and try again.
 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
   = -- Rewrite the two types and try again
-    do { (redn1@(Reduction _ _ xi1), rewriters1) <- rewrite ev ps_ty1
-       ; (redn2@(Reduction _ _ xi2), rewriters2) <- rewrite ev ps_ty2
-       ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
+    do { (redn1@(Reduction _ xi1), rewriters1) <- rewrite ev ps_ty1
+       ; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ps_ty2
+       ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped
+                     (ps_ty1,redn1) (ps_ty2,redn2)
        ; traceTcS "can_eq_nc: go round again" (ppr new_ev $$ ppr xi1 $$ ppr xi2)
        ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
@@ -631,12 +632,12 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
          -- through newtypes is tantamount to using their constructors.
        ; recordUsedGREs gres
 
-       ; let redn1 = mkReduction ty1 (mkDehydrateCo co1) ty1'
+       ; let redn1 = mkReduction (mkDehydrateCo co1) ty1'
              -- TODO: eliminate dehydration
 
 
        ; new_ev <- rewriteEqEvidence emptyRewriterSet ev' swapped
-                     redn1 (mkReflRedn ps_ty2)
+                     (ty1, redn1) (ps_ty2,mkReflRedn ps_ty2)
 
        ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
 
@@ -707,8 +708,8 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
                                            , ppr ty1 <+> text "|>" <+> ppr co1
                                            , ppr ps_ty2 ])
        ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
-                      (mkGReflLeftRedn ty1 co1)
-                      (mkReflRedn ps_ty2)
+                      (mkCastTy ty1 co1, mkGReflLeftRedn ty1 co1)
+                      (ps_ty2, mkReflRedn ps_ty2)
        ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
 
 ------------------------
@@ -1270,7 +1271,8 @@ canEqFailure ev ReprEq ty1 ty2
             -- new equalities become available
        ; traceTcS "canEqFailure with ReprEq" $
          vcat [ ppr ev, ppr redn1, ppr redn2 ]
-       ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
+       ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped
+                     (ty1,redn1) (ty2,redn2)
        ; continueWith (mkIrredCt ReprEqReason new_ev) }
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
@@ -1281,7 +1283,8 @@ canEqHardFailure ev ty1 ty2
   = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2)
        ; (redn1, rewriters1) <- rewriteForErrors ev ty1
        ; (redn2, rewriters2) <- rewriteForErrors ev ty2
-       ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
+       ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped
+                     (ty1,redn1) (ty2,redn2)
        ; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
 
 {-
@@ -1468,7 +1471,8 @@ canEqCanLHSHetero ev swapped lhs1 ki1 xi2 ki2
 
        ; traceTcS "Hetero equality gives rise to kind equality"
            (ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
-       ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
+       ; type_ev <- rewriteEqEvidence rewriters ev swapped
+                      (xi1,lhs_redn) (xi2,rhs_redn)
 
        ; emitWorkNC [type_ev]  -- delay the type equality until after we've finished
                                -- the kind equality, which may unlock things
@@ -1627,7 +1631,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
     finish_with_swapping
       = do { let lhs1_redn = mkGReflRightMRedn lhs1_ty sym_mco
                  lhs2_redn = mkGReflLeftMRedn  lhs2_ty mco
-           ; new_ev <-rewriteEqEvidence emptyRewriterSet ev swapped lhs1_redn lhs2_redn
+           ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
+                       (lhs1_ty, lhs1_redn) (mkCastTyMCo lhs2_ty mco, lhs2_redn)
            ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
 
     put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq
@@ -1771,8 +1776,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
          --           co' = <Int>
          new_ev <- if isReflDCo (reductionDCoercion rhs_redn)
                    then return ev
-                   else rewriteEqEvidence emptyRewriterSet ev swapped
-                            (mkReflRedn (mkTyVarTy tv)) rhs_redn
+                   else let lhs = mkTyVarTy tv
+                            in rewriteEqEvidence emptyRewriterSet ev swapped
+                            (lhs, mkReflRedn lhs) (rhs, rhs_redn)
 
        ; let tv_ty     = mkTyVarTy tv
              final_rhs = reductionReducedType rhs_redn
@@ -1848,8 +1854,8 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
 
             PuOK rhs_redn _
               -> do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
-                                   (mkReflRedn lhs_ty)
-                                   rhs_redn
+                                   (lhs_ty, mkReflRedn lhs_ty)
+                                   (rhs, rhs_redn)
 
                     -- Important: even if the coercion is Refl,
                     --   * new_ev has reductionReducedType on the RHS
@@ -1867,9 +1873,10 @@ swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
 -- mentions alpha, it would not be a canonical constraint as-is.
 -- We want to flip it to (F tys ~ a), whereupon it is canonical
 swapAndFinish ev eq_rel swapped lhs_ty can_rhs
-  = do { new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
-                       (mkReflRedn (canEqLHSType can_rhs))
-                       (mkReflRedn lhs_ty)
+  = do { let rhs = canEqLHSType can_rhs
+       ; new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
+                       (rhs, mkReflRedn rhs)
+                       (lhs_ty, mkReflRedn lhs_ty)
        ; interactEq (EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
                           , eq_lhs = can_rhs, eq_rhs = lhs_ty }) }
 
@@ -1883,9 +1890,10 @@ tryIrredInstead :: CheckTyEqResult -> CtEvidence -> SwapFlag
 -- This is not very important, and only affects error reporting.
 tryIrredInstead reason ev swapped lhs rhs
   = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)
+       ; let lhs_ty = canEqLHSType lhs
        ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
-                       (mkReflRedn (canEqLHSType lhs))
-                       (mkReflRedn rhs)
+                       (lhs_ty, mkReflRedn lhs_ty)
+                       (rhs, mkReflRedn rhs)
        ; solveIrredEquality (NonCanonicalReason reason) new_ev }
 
 -----------------------
@@ -2361,8 +2369,8 @@ rewriteEqEvidence :: RewriterSet        -- New rewriters
                   -> CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
                                         --              or orhs ~ olhs (swapped)
                   -> SwapFlag
-                  -> Reduction          -- lhs_co :: olhs ~ nlhs
-                  -> Reduction          -- rhs_co :: orhs ~ nrhs
+                  -> (Type, Reduction)  -- lhs_co :: olhs ~ nlhs
+                  -> (Type, Reduction)  -- rhs_co :: orhs ~ nrhs
                   -> TcS CtEvidence     -- Of type nlhs ~ nrhs
 -- With reductions (Reduction lhs_co nlhs) (Reduction rhs_co nrhs),
 -- rewriteEqEvidence yields, for a given equality (Given g olhs orhs):
@@ -2379,7 +2387,8 @@ rewriteEqEvidence :: RewriterSet        -- New rewriters
 --      w : orhs ~ olhs = rhs_co ; sym w1 ; sym lhs_co
 --
 -- It's all a form of rewriteEvidence, specialised for equalities
-rewriteEqEvidence new_rewriters old_ev swapped lhs_redn@(Reduction _ lhs_dco nlhs) rhs_redn@(Reduction _ rhs_dco nrhs)
+rewriteEqEvidence new_rewriters old_ev swapped (olhs, lhs_redn@(Reduction lhs_dco nlhs))
+                                               (orhs, rhs_redn@(Reduction rhs_dco nrhs))
   | NotSwapped <- swapped
   , isReflDCo lhs_dco      -- See Note [Rewriting with Refl]
   , isReflDCo rhs_dco
@@ -2415,8 +2424,8 @@ rewriteEqEvidence new_rewriters old_ev swapped lhs_redn@(Reduction _ lhs_dco nlh
   where
     new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
     loc      = ctEvLoc old_ev
-    lhs_co = mkHydrateReductionDCoercion (ctEvRole old_ev) lhs_redn
-    rhs_co = mkHydrateReductionDCoercion (ctEvRole old_ev) rhs_redn
+    lhs_co = mkHydrateReductionDCoercion (ctEvRole old_ev) olhs lhs_redn
+    rhs_co = mkHydrateReductionDCoercion (ctEvRole old_ev) orhs rhs_redn
 
 {-
 **********************************************************************
@@ -2675,7 +2684,7 @@ final_qci_check work_ct eq_rel lhs rhs
             ; case res of
                 OneInst { cir_mk_ev = mk_ev }
                   -> do { ev' <- rewriteEqEvidence emptyRewriterSet ev IsSwapped
-                                      (mkReflRedn rhs) (mkReflRedn lhs)
+                                      (rhs, mkReflRedn rhs) (lhs, mkReflRedn lhs)
                         ; chooseInstance ev' (res { cir_mk_ev = mk_eq_ev cls tys mk_ev }) }
                 _ -> do { traceTcS "final_qci_check:3" (ppr work_ct)
                         ; continueWith work_ct }}


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -729,12 +729,11 @@ lookupFamAppInert rewrite_pred fam_tc tys
   = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
        ; return (lookup_inerts inert_funeqs) }
   where
-    fam_app = mkTyConApp fam_tc tys
     lookup_inerts inert_funeqs
       | Just ecl <- findFunEq inert_funeqs fam_tc tys
       , Just (EqCt { eq_ev = ctev, eq_rhs = rhs })
           <- find (rewrite_pred . eqCtFlavourRole) ecl
-      = Just (mkReduction fam_app (mkDehydrateCo (ctEvCoercion ctev)) rhs -- SLD TODO: avoid dehydrating?
+      = Just (mkReduction (mkDehydrateCo (ctEvCoercion ctev)) rhs -- SLD TODO: avoid dehydrating?
              ,ctEvFlavourRole ctev)
       | otherwise = Nothing
 
@@ -785,7 +784,7 @@ lookupFamAppCache fam_tc tys
            Nothing -> return Nothing }
 
 extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
-extendFamAppCache tc xi_args stuff@(Reduction _ _ ty)
+extendFamAppCache tc xi_args stuff@(Reduction _ ty)
   = do { dflags <- getDynFlags
        ; when (gopt Opt_FamAppCache dflags) $
     do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args
@@ -1877,7 +1876,7 @@ matchFamTcM tycon args
        ; return match_fam_result }
   where
     ppr_res Nothing = text "Match failed"
-    ppr_res (Just (Reduction _ co ty))
+    ppr_res (Just (Reduction co ty))
       = hang (text "Match succeeded:")
           2 (vcat [ text "Rewrites to:" <+> ppr ty
                   , text "Coercion:" <+> ppr co ])


=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -93,12 +93,10 @@ runRewriteCtEv ev
 runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
 runRewrite loc flav eq_rel thing_inside
   = do { rewriters_ref <- newTcRef emptyRewriterSet
-       ; followed_ref <- newTcRef emptyVarSet
        ; let rmode = RE { re_loc  = loc
                         , re_flavour = flav
                         , re_eq_rel = eq_rel
-                        , re_rewriters = rewriters_ref
-                        , re_followed = followed_ref }
+                        , re_rewriters = rewriters_ref }
        ; res <- runRewriteM thing_inside rmode
        ; rewriters <- readTcRef rewriters_ref
        ; return (res, rewriters) }
@@ -155,26 +153,6 @@ bumpDepth (RewriteM thing_inside)
       { let !env' = env { re_loc = bumpCtLocDepth (re_loc env) }
       ; thing_inside env' }
 
--- | Register that we followed a metavariable.
---
--- See Wrinkle 2 in Note [The Hydration invariant in the rewriter].
-registerFollowedTyVar :: TcTyVar -> RewriteM ()
-registerFollowedTyVar tv
-  = mkRewriteM $ \ (RE { re_followed = followed_ref }) ->
-      updTcRef followed_ref (`extendVarSet` tv)
-
--- | Run an inner computation, tracking which type variables it has followed.
---
--- See Wrinkle 2 in Note [The Hydration invariant in the rewriter].
-trackFollowedTyVars :: RewriteM a -> RewriteM (a, TyVarSet)
-trackFollowedTyVars thing_inside
-  = mkRewriteM $ \ re@(RE { re_followed = followed_ref }) ->
-    do { inner_ref <- newTcRef emptyVarSet
-       ; res <- runRewriteM thing_inside (re { re_followed = inner_ref })
-       ; inner_followed <- readTcRef inner_ref
-       ; updTcRef followed_ref (unionVarSet inner_followed)
-       ; return (res, inner_followed ) }
-
 -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
 -- Precondition: the CtEvidence is a CtWanted of an equality
 recordRewriter :: CtEvidence -> RewriteM ()
@@ -246,7 +224,6 @@ rewrite ev ty
        ; result@(redn, _) <- runRewriteCtEv ev (rewrite_one ty)
        ; traceTcS "rewrite }" $
           vcat [ text "ty:" <+> ppr ty
-               , text "ty':" <+> ppr (reductionOriginalType redn)
                , text "dco:" <+> ppr (reductionDCoercion redn)
                , text "xi:" <+> ppr (reductionReducedType redn) ]
        ; return result }
@@ -265,7 +242,7 @@ rewriteForErrors ev ty
        ; traceTcS "rewriteForErrors }" (ppr $ reductionReducedType redn)
        ; return $ case ctEvEqRel ev of
            NomEq -> result
-           ReprEq -> (mkSubRedn redn, rewriters) }
+           ReprEq -> (mkSubRedn ty redn, rewriters) }
 
 -- See Note [Rewriting]
 rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
@@ -282,7 +259,7 @@ rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
 -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
 rewriteArgsNom ev tc tys
   = do { traceTcS "rewriteArgsNom {" (vcat (map ppr tys))
-       ; (ArgsReductions redns@(Reductions _ _ tys') kind_dco, rewriters)
+       ; (ArgsReductions redns@(Reductions _ tys') kind_dco, rewriters)
            <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys)
        ; massert (isReflMCo kind_dco)
        ; traceTcS "rewriteArgsNom }" (vcat (map ppr tys'))
@@ -595,10 +572,10 @@ rewrite_args_fast orig_tys
 
     iterate :: [Type] -> RewriteM Reductions
     iterate (ty : tys) = do
-      Reduction  ty'  co  xi  <- rewrite_one ty
-      Reductions tys' cos xis <- iterate tys
-      pure $ Reductions (ty' : tys') (co : cos) (xi : xis)
-    iterate [] = pure $ Reductions [] [] []
+      Reduction  co  xi  <- rewrite_one ty
+      Reductions cos xis <- iterate tys
+      pure $ Reductions (co : cos) (xi : xis)
+    iterate [] = pure $ Reductions [] []
 
     {-# INLINE finish #-}
     finish :: Reductions -> ArgsReductions
@@ -617,7 +594,7 @@ rewrite_args_slow binders inner_ki fvs roles tys
          -- See Note [The Reduction type] in GHC.Core.Reduction,
          -- and Note [The Hydration invariant] in GHC.Core.Coercion.
          -- Relevant test case: T13333.
-       ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args }
+       ; return $ simplifyArgsWorker binders inner_ki fvs roles tys rewritten_args }
   where
     {-# INLINE rw #-}
     rw :: Role -> Type -> RewriteM Reduction
@@ -676,8 +653,8 @@ rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
              res_rep = getRuntimeRep (reductionReducedType res_redn)
 
        ; ( w_redn
-         , Reduction arg_rep arg_rep_dco arg_rep_xi
-         , Reduction res_rep res_rep_dco res_rep_xi
+         , Reduction arg_rep_dco arg_rep_xi
+         , Reduction res_rep_dco res_rep_xi
          ) <- setEqRel NomEq $
                 liftA3 (,,) (rewrite_one mult)
                             (rewrite_one arg_rep)
@@ -735,20 +712,10 @@ rewrite_co co = liftTcS $ zonkCo co
 
 -- | Rewrite a reduction, composing the resulting coercions.
 rewrite_reduction :: Reduction -> RewriteM Reduction
-rewrite_reduction redn0@(Reduction _ _ xi)
+rewrite_reduction redn0@(Reduction _ xi)
   = do { redn <- bumpDepth $ rewrite_one xi
        ; return $ redn0 `mkTransRedn` redn }
 
--- | Zonk the LHS of a 'Reduction' to enforce the Hydration
--- invariant of Note [The Hydration invariant] in GHC.Core.Coercion.
---
--- See Wrinkle 2 of Note [The Hydration invariant in the rewriter]
--- for why this is necessary.
-zonk_redn_lhs :: Reduction -> RewriteM Reduction
-zonk_redn_lhs (Reduction lhs dco rhs)
-  = do { lhs <- liftTcS $ zonkTcType lhs
-       ; return $ Reduction lhs dco rhs }
-
 -- rewrite (nested) AppTys
 rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
 -- commoning up nested applications allows us to look up the function's kind
@@ -769,12 +736,12 @@ rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
 rewrite_app_ty_args redn []
   -- this will be a common case when called from rewrite_fam_app, so shortcut
   = return redn
-rewrite_app_ty_args fun_redn@(Reduction fun_ty fun_co fun_xi) more_arg_tys
+rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) more_arg_tys
   = case tcSplitTyConApp_maybe fun_xi of
       Just (tc, xis) ->
         do { let tc_roles  = tyConRolesRepresentational tc
                  arg_roles = Inf.dropList xis tc_roles
-           ; ArgsReductions (Reductions more_arg_tys arg_cos arg_xis) kind_co
+           ; ArgsReductions (Reductions arg_cos arg_xis) kind_co
                <- rewrite_vector (typeKind fun_xi) arg_roles more_arg_tys
 
              -- We start with a reduction of the form
@@ -789,15 +756,14 @@ rewrite_app_ty_args fun_redn@(Reduction fun_ty fun_co fun_xi) more_arg_tys
              -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m
 
            ; eq_rel <- getEqRel
-           ; let app_ty = mkAppTys fun_ty more_arg_tys
-                 app_xi = mkTyConApp tc (xis ++ arg_xis)
+           ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
                  app_co = case eq_rel of
                    NomEq  -> mkAppDCos fun_co arg_cos
                    ReprEq -> mkAppDCos fun_co (mkReflDCos more_arg_tys)
                              `mkTransDCo`
                              mkTyConAppDCo (mkReflDCos xis ++ arg_cos)
 
-           ; return $ homogeniseRedn (mkReduction app_ty app_co app_xi) kind_co }
+           ; return $ homogeniseRedn (mkReduction app_co app_xi) kind_co }
       Nothing ->
         do { ArgsReductions redns kind_co
                <- rewrite_vector (typeKind fun_xi) (Inf.repeat Nominal) more_arg_tys
@@ -810,7 +776,7 @@ rewrite_ty_con_app tc tys
                      | otherwise       = Just $ tyConRolesX role tc
        ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys
        ; return $ homogeniseRedn
-                    (mkTyConAppRedn_MightBeSynonym role tc redns)
+                    (mkTyConAppRedn_MightBeSynonym role tc tys redns)
                     kind_co }
 {-# INLINE rewrite_ty_con_app #-}
 
@@ -973,13 +939,12 @@ rewrite_exact_fam_app tc tys
        ; case result1 of
              -- Don't use the cache;
              -- See Note [rewrite_exact_fam_app performance]
-         { Just redn -> finish (Don'tAddToCache { followed_arg_tvs = emptyVarSet }) redn
+         { Just redn -> finish Don'tAddToCache redn
          ; Nothing ->
 
         -- That didn't work. So reduce the arguments, in STEP 2.
-    do { ( ArgsReductions redns@(Reductions tys' _ xis) kind_co
-         , followed_args) <-
-            trackFollowedTyVars $ setEqRel NomEq $ rewrite_args_tc tc Nothing tys
+    do { (ArgsReductions redns@(Reductions _ xis) kind_co) <-
+            setEqRel NomEq $ rewrite_args_tc tc Nothing tys
 
          -- If we manage to rewrite the type family application after
          -- rewriting the arguments, we will need to compose these
@@ -1002,14 +967,6 @@ rewrite_exact_fam_app tc tys
                    (args_redn `mkTransRedn` redn)
                    kind_co
 
-             add_to_cache, don't_add_to_cache :: AddToCache
-             add_to_cache =
-                RewroteArgsAddToCache
-                { finish_arg_tys = tys'
-                , followed_arg_tvs = followed_args }
-             don't_add_to_cache =
-                Don'tAddToCache
-                { followed_arg_tvs = followed_args }
              give_up :: Reduction
              give_up = homogenise $ mkReflRedn reduced
                where reduced = mkTyConApp tc xis
@@ -1026,16 +983,16 @@ rewrite_exact_fam_app tc tys
                        -- Don't add something to the cache if the reduction
                        -- contains a coercion hole.
                        | inert_flavour == Given
-                       = add_to_cache
+                       = RewroteArgsAddToCache
                        | otherwise
-                       = don't_add_to_cache
+                       = Don'tAddToCache
                ; finish use_cache (homogenise downgraded_redn) }
              where
                inert_role      = eqRelRole inert_eq_rel
                role            = eqRelRole eq_rel
                !downgraded_redn
                  | inert_role == Nominal && role == Representational
-                 = mkSubRedn redn
+                 = mkSubRedn (mkTyConApp tc xis) redn
                  | otherwise
                  = redn
 
@@ -1044,7 +1001,7 @@ rewrite_exact_fam_app tc tys
          -- inerts didn't work. Try to reduce again, in STEP 4.
     do { result3 <- try_to_reduce tc xis tc_rewriters
        ; case result3 of
-           Just redn -> finish add_to_cache (homogenise redn)
+           Just redn -> finish RewroteArgsAddToCache (homogenise redn)
            -- we have made no progress at all: STEP 5 (GIVEUP).
            _         -> return give_up }}}}}
   where
@@ -1056,25 +1013,18 @@ rewrite_exact_fam_app tc tys
            -> RewriteM Reduction
     finish use_cache redn
       = do { -- rewrite the result: FINISH 1
-             (rewritten_redn, followed_tvs) <- trackFollowedTyVars $ rewrite_reduction redn
-           ; final_redn <-
-               if isEmptyVarSet followed_tvs && isEmptyVarSet (followed_arg_tvs use_cache)
-               then return rewritten_redn
-               else zonk_redn_lhs rewritten_redn --  See Wrinkle 2 in Note [The Hydration invariant in the rewriter]
+             final_redn <- rewrite_reduction redn
            ; case use_cache of
            { Don'tAddToCache {} -> return final_redn
-           ; RewroteArgsAddToCache { finish_arg_tys = arg_tys } ->
+           ; RewroteArgsAddToCache ->
              -- extend the cache: FINISH 2
         do { eq_rel <- getEqRel
            ; when (eq_rel == NomEq) $
                -- the cache only wants Nominal eqs
-               liftTcS $ extendFamAppCache tc arg_tys final_redn
+               liftTcS $ extendFamAppCache tc tys final_redn
                  -- This will sometimes duplicate an inert in the cache,
                  -- but avoiding doing so had no impact on performance, and
                  -- it seems easier not to weed out that special case.
-                 --
-                 -- NB: it's important to use 'arg_tys' and not just 'tys' here.
-                 -- See Wrinkle 3 in Note [The Hydration invariant in the rewriter].
            ; return final_redn } } }
     {-# INLINE finish #-}
 
@@ -1085,15 +1035,9 @@ data AddToCache
   --
   -- See Note [rewrite_exact_fam_app performance].
   = Don'tAddToCache
-      { followed_arg_tvs :: TyVarSet }
   -- | We rewrote the arguments. We add the type family application,
   -- with rewritten arguments, to the cache.
-  --
-  -- It's important to use the rewritten arguments when adding to the
-  -- cache. See Wrinkle 3 in Note [The Hydration invariant in the rewriter].
   | RewroteArgsAddToCache
-      { finish_arg_tys   :: [Xi]
-      , followed_arg_tvs :: TyVarSet }
 
 -- Returned coercion is input ~r output, where r is the role in the RewriteM monad
 -- See Note [How to normalise a family application]
@@ -1122,7 +1066,7 @@ try_to_reduce tc tys tc_rewriters
               -- common NomEq case
            ; case eq_rel of
                NomEq  -> return redn
-               ReprEq -> return $ mkSubRedn redn }
+               ReprEq -> return $ mkSubRedn (mkTyConApp tc tys) redn }
 
 -- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application
 -- headed by the given 'TyCon`.
@@ -1217,10 +1161,6 @@ rewrite_tyvar1 tv
        ; case mb_ty of
            Just ty -> do { traceRewriteM "Following filled tyvar"
                              (ppr tv <+> equals <+> ppr ty)
-                         ; registerFollowedTyVar tv
-                         -- Register that we followed a metavariable.
-                         --
-                         -- See Wrinkle 2 in Note [The Hydration invariant in the rewriter].
                          ; return $ RTRFollowedMeta ty }
            Nothing -> do { traceRewriteM "Unfilled tyvar" (pprTyVar tv)
                          ; fr <- getFlavourRole
@@ -1255,7 +1195,7 @@ rewrite_tyvar2 tv fr@(_, eq_rel)
                             (NomEq, NomEq)  -> rewriting_dco1
                             (NomEq, ReprEq) -> mkSubDCo lhs_ty rewriting_dco1 rhs_ty
 
-                    ; return $ RTRFollowedInert $ mkReduction lhs_ty rewriting_dco rhs_ty }
+                    ; return $ RTRFollowedInert $ mkReduction rewriting_dco rhs_ty }
 
            _other -> return RTRNotFollowed }
   where


=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -295,11 +295,6 @@ data RewriteEnv
        -- See Note [Rewriter EqRels] in GHC.Tc.Solver.Rewrite
        , re_rewriters :: !(TcRef RewriterSet)
        -- ^ See Note [Wanteds rewrite Wanteds]
-
-       , re_followed :: !(TcRef TyVarSet)
-       -- ^ Used to keep track of which metavariables we have followed.
-       --
-       -- See Note [The Hydration invariant in the rewriter] in GHC.Tc.Solver.Rewrite.
        }
 -- RewriteEnv is mostly used in @GHC.Tc.Solver.Rewrite@, but it is defined
 -- here so that it can also be passed to rewriting plugins.


=====================================
compiler/GHC/Types/Id/Make.hs
=====================================
@@ -1061,7 +1061,7 @@ dataConSrcToImplBang bang_opts fam_envs arg_ty
     else case mb_redn of
            Nothing   -> HsUnpack Nothing
            Just redn -> HsUnpack $ Just $
-                        mkHydrateReductionDCoercion Representational redn
+                        mkHydrateReductionDCoercion Representational (scaledThing arg_ty) redn
 
   | otherwise -- Record the strict-but-no-unpack decision
   = HsStrict False


=====================================
testsuite/tests/dcoercion/DCo_Phantom.hs
=====================================
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies,
+{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies,
              UndecidableInstances, ConstraintKinds #-}
 module DCo_Phantom where
 


=====================================
testsuite/tests/dcoercion/DCo_Phantom.stderr
=====================================
@@ -1,5 +1,5 @@
 
-DCo_Phantom.hs:35:11: warning: [-Wtyped-holes (in -Wdefault)]
+DCo_Phantom.hs:35:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
     • Found hole:
         _a :: [Integer] -> Sorted (O ('NLogN 2 0)) (O N) 'True Integer
       Or perhaps ‘_a’ is mis-spelled, or not in scope


=====================================
testsuite/tests/dcoercion/DCo_Specialise.hs
=====================================
@@ -4,6 +4,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 module DCo_Specialise ( rnStmts1 ) where
 


=====================================
testsuite/tests/dcoercion/DCo_T15703_aux.hs
=====================================
@@ -1,5 +1,6 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
@@ -8,7 +9,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e07c825ebf2028273066e8201de4ffec97ab806

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e07c825ebf2028273066e8201de4ffec97ab806
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230512/6bdd280e/attachment-0001.html>


More information about the ghc-commits mailing list