[Git][ghc/ghc][wip/amg/dcoercion] WIP: remove LHS type in Reduction
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri May 12 23:15:47 UTC 2023
sheaf pushed to branch wip/amg/dcoercion at Glasgow Haskell Compiler / GHC
Commits:
43c4c1e6 by sheaf at 2023-05-13T01:15:29+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,8 @@ 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 (HydrateDCo _ _ (ForAllDCo tv kind_co _) rhs)
+ = Just $ mkHydrateDCo Nominal (tyVarKind tv) kind_co (Just $ typeKind rhs)
go (SelFun fs) (FunCo _ _ _ w arg res)
= Just (getNthFun fs w arg res)
@@ -1820,7 +1822,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 +2085,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/43c4c1e6607ec098b8b7806e9e62ed3c4251e1e1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/43c4c1e6607ec098b8b7806e9e62ed3c4251e1e1
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/683b5083/attachment-0001.html>
More information about the ghc-commits
mailing list