[Git][ghc/ghc][wip/simplifier-tweaks] 3 commits: Better documentation
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jul 5 11:59:47 UTC 2023
Simon Peyton Jones pushed to branch wip/simplifier-tweaks at Glasgow Haskell Compiler / GHC
Commits:
028734fc by Simon Peyton Jones at 2023-07-05T12:47:48+01:00
Better documentation
- - - - -
b02c67b7 by Simon Peyton Jones at 2023-07-05T12:48:09+01:00
Improve pretty printing of InstCo
- - - - -
99d011f8 by Simon Peyton Jones at 2023-07-05T12:48:44+01:00
More improvements
* Make opt_co4 (SelCo cs Refl) work properly. It wasn't!
* Deal well with (ax ty ; sym (ax ty)). Bizarrely that didn't work.
I just put the ax/sym-ax rule first.
* Make (mkInstCo Refl ty) work. Bizarrely it didn't!
- - - - -
6 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Opt/Simplify/Env.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Iface/Type.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -37,7 +37,7 @@ module GHC.Core.Coercion (
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo,
- mkSelCo, getNthFun, getNthFromType, mkLRCo,
+ mkSelCo, mkSelCoResRole, getNthFun, getNthFromType, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
mkNakedFunCo,
@@ -556,20 +556,28 @@ splitFunCo_maybe (FunCo { fco_arg = arg, fco_res = res }) = Just (arg, res)
splitFunCo_maybe _ = Nothing
splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
-splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
-splitForAllCo_maybe _ = Nothing
+splitForAllCo_maybe (ForAllCo tv k_co co)
+ = Just (tv, k_co, co)
+splitForAllCo_maybe co
+ | Just (ty, r) <- isReflCo_maybe co
+ , Just (tcv, body_ty) <- splitForAllTyCoVar_maybe ty
+ = Just (tcv, mkNomReflCo (varType tcv), mkReflCo r body_ty)
+splitForAllCo_maybe _
+ = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
-splitForAllCo_ty_maybe (ForAllCo tv k_co co)
- | isTyVar tv = Just (tv, k_co, co)
-splitForAllCo_ty_maybe _ = Nothing
+splitForAllCo_ty_maybe co
+ | Just stuff@(tv,_,_) <- splitForAllCo_maybe co
+ , isTyVar tv = Just stuff
+ | otherwise = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
-splitForAllCo_co_maybe (ForAllCo cv k_co co)
- | isCoVar cv = Just (cv, k_co, co)
-splitForAllCo_co_maybe _ = Nothing
+splitForAllCo_co_maybe co
+ | Just stuff@(cv,_,_) <- splitForAllCo_maybe co
+ , isCoVar cv = Just stuff
+ | otherwise = Nothing
-------------------------------------------------------
-- and some coercion kind stuff
@@ -1166,13 +1174,7 @@ mkSelCo_maybe cs co
go cs co
| Just (ty, r) <- isReflCo_maybe co
- = Just (mkReflCo (mk_res_role r cs) (getNthFromType cs ty))
- where
- -- The result role is not just the role of co!
- -- c.f. the SelCo case of coercionRole
- mk_res_role _ SelForAll = Nominal
- mk_res_role _ (SelTyCon _ r') = r'
- mk_res_role r (SelFun fs) = funRole r fs
+ = Just (mkReflCo (mkSelCoResRole cs r) (getNthFromType cs ty))
go SelForAll (ForAllCo _ kind_co _)
= Just kind_co
@@ -1223,6 +1225,14 @@ mkSelCo_maybe cs co
good_call _ = False
+mkSelCoResRole :: CoSel -> Role -> Role
+-- What is the role of (SelCo cs co), if co has role 'r'?
+-- It is not just 'r'!
+-- c.f. the SelCo case of coercionRole
+mkSelCoResRole SelForAll _ = Nominal
+mkSelCoResRole (SelTyCon _ r') _ = r'
+mkSelCoResRole (SelFun fs) r = funRole r fs
+
-- | Extract the nth field of a FunCo
getNthFun :: FunSel
-> a -- ^ multiplicity
@@ -1241,11 +1251,14 @@ mkLRCo lr co
= LRCo lr co
-- | Instantiates a 'Coercion'.
+-- Works for both tyvar and covar
mkInstCo :: Coercion -> CoercionN -> Coercion
-mkInstCo (ForAllCo tcv _kind_co body_co) co
- | Just (arg, _) <- isReflCo_maybe co
- -- works for both tyvar and covar
- = substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
+mkInstCo co_fun co_arg
+ | Just (tcv, kind_co, body_co) <- splitForAllCo_maybe co_fun
+ , Just (arg, _) <- isReflCo_maybe co_arg
+ = assertPpr (isReflexiveCo kind_co) (ppr co_fun $$ ppr co_arg) $
+ -- If the arg is Refl, then kind_co must be reflexive too
+ substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
mkInstCo co arg = InstCo co arg
-- | Given @ty :: k1@, @co :: k1 ~ k2@,
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -23,7 +23,7 @@ import GHC.Core.Unify
import GHC.Types.Var.Set
import GHC.Types.Var.Env
-import GHC.Types.Unique.Set
+-- import GHC.Types.Unique.Set
import GHC.Data.Pair
import GHC.Data.List.SetOps ( getNth )
@@ -136,42 +136,48 @@ optCoercion opts env co
{-
= pprTrace "optCoercion {" (text "Co:" <> ppr (coercionSize co)) $
let result = optCoercion' env co in
- pprTrace "optCoercion }" (vcat [ text "Co:" <+> ppr (coercionSize co)
- , text "Optco:" <+> ppr (coercionSize result) ]) $
+ pprTrace "optCoercion }"
+ (vcat [ text "Co:" <+> ppr (coercionSize co)
+ , text "Optco:" <+> ppWhen (isReflCo result) (text "(refl)")
+ <+> ppr (coercionSize result) ]) $
result
-}
| otherwise
= substCo env co
-
optCoercion' :: Subst -> Coercion -> NormalCo
optCoercion' env co
| debugIsOn
= let out_co = opt_co1 lc False co
(Pair in_ty1 in_ty2, in_role) = coercionKindRole co
(Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
+
+ details = vcat [ text "in_co:" <+> ppr co
+ , text "in_ty1:" <+> ppr in_ty1
+ , text "in_ty2:" <+> ppr in_ty2
+ , text "out_co:" <+> ppr out_co
+ , text "out_ty1:" <+> ppr out_ty1
+ , text "out_ty2:" <+> ppr out_ty2
+ , text "in_role:" <+> ppr in_role
+ , text "out_role:" <+> ppr out_role
+-- , vcat $ map ppr_one $ nonDetEltsUniqSet $ coVarsOfCo co
+-- , text "subst:" <+> ppr env
+ ]
in
+ warnPprTrace (not (isReflCo out_co) && isReflexiveCo out_co)
+ "optCoercion: reflexive but not refl" details $
assertPpr (substTyUnchecked env in_ty1 `eqType` out_ty1 &&
substTyUnchecked env in_ty2 `eqType` out_ty2 &&
in_role == out_role)
- (hang (text "optCoercion changed types!")
- 2 (vcat [ text "in_co:" <+> ppr co
- , text "in_ty1:" <+> ppr in_ty1
- , text "in_ty2:" <+> ppr in_ty2
- , text "out_co:" <+> ppr out_co
- , text "out_ty1:" <+> ppr out_ty1
- , text "out_ty2:" <+> ppr out_ty2
- , text "in_role:" <+> ppr in_role
- , text "out_role:" <+> ppr out_role
- , vcat $ map ppr_one $ nonDetEltsUniqSet $ coVarsOfCo co
- , text "subst:" <+> ppr env ]))
- out_co
-
- | otherwise = opt_co1 lc False co
+ (hang (text "optCoercion changed types!") 2 details) $
+ out_co
+
+ | otherwise
+ = opt_co1 lc False co
where
lc = mkSubstLiftingContext env
- ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv)
+-- ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv)
type NormalCo = Coercion
@@ -394,11 +400,17 @@ opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo _ eta _))
-- works for both tyvar and covar
= opt_co4_wrap env sym rep Nominal eta
-opt_co4 env sym rep r (SelCo n co)
- | Just nth_co <- case (co', n) of
- (TyConAppCo _ _ cos, SelTyCon n _) -> Just (cos `getNth` n)
- (FunCo _ _ _ w co1 co2, SelFun fs) -> Just (getNthFun fs w co1 co2)
- (ForAllCo _ eta _, SelForAll) -> Just eta
+-- So the /input/ coercion isn't ForAllCo or Refl;
+-- instead look at the /output/ coercion
+opt_co4 env sym rep r (SelCo cs co)
+ | Just (ty, co_role) <- isReflCo_maybe co'
+ = mkReflCo (chooseRole rep (mkSelCoResRole cs co_role))
+ (getNthFromType cs ty)
+
+ | Just nth_co <- case (co', cs) of
+ (TyConAppCo _ _ cos, SelTyCon n _) -> Just (cos `getNth` n)
+ (FunCo _ _ _ w co1 co2, SelFun fs) -> Just (getNthFun fs w co1 co2)
+ (ForAllCo _ eta _, SelForAll) -> Just eta
_ -> Nothing
= if rep && (r == Nominal)
-- keep propagating the SubCo
@@ -406,7 +418,7 @@ opt_co4 env sym rep r (SelCo n co)
else nth_co
| otherwise
- = wrapRole rep r $ SelCo n co'
+ = wrapRole rep r $ SelCo cs co'
where
co' = opt_co1 env sym co
@@ -601,7 +613,6 @@ opt_univ env sym prov role oty1 oty2
(env', tv1', eta') = optForAllCoBndr env sym tv1 eta
in
mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
-
| Just (cv1, ty1) <- splitForAllCoVar_maybe oty1
, Just (cv2, ty2) <- splitForAllCoVar_maybe oty2
-- NB: prov isn't interesting here either
@@ -835,6 +846,32 @@ opt_trans_rule is co1 co2
-- Push transitivity inside axioms
opt_trans_rule is co1 co2
+ -- TrPushAxSym/TrPushSymAx
+ -- Put this first! Otherwise we get
+ -- newtype N a = MkN a
+ -- axN :: forall a. N a ~ a
+ -- Now consider (axN ty ; sym (axN ty))
+ -- If we put TrPushSymAxR first, we'll get
+ -- (axN ty ; sym (axN ty)) :: N ty ~ N ty -- Obviously Refl
+ -- --> axN (sym (axN ty)) :: N ty ~ N ty -- Very stupid
+ | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
+ , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
+ , con1 == con2
+ , ind1 == ind2
+ , sym1 == not sym2
+ , let branch = coAxiomNthBranch con1 ind1
+ qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
+ lhs = coAxNthLHS con1 ind1
+ rhs = coAxBranchRHS branch
+ pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
+ , all (`elemVarSet` pivot_tvs) qtvs
+ = fireTransRule "TrPushAxSym" co1 co2 $
+ if sym2
+ -- TrPushAxSym
+ then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
+ -- TrPushSymAx
+ else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
+
-- See Note [Push transitivity inside axioms] and
-- Note [Push transitivity inside newtype axioms only]
-- TrPushSymAxR
@@ -869,24 +906,6 @@ opt_trans_rule is co1 co2
, let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
= fireTransRule "TrPushAxL" co1 co2 newAxInst
- -- TrPushAxSym/TrPushSymAx
- | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
- , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
- , con1 == con2
- , ind1 == ind2
- , sym1 == not sym2
- , let branch = coAxiomNthBranch con1 ind1
- qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
- lhs = coAxNthLHS con1 ind1
- rhs = coAxBranchRHS branch
- pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
- , all (`elemVarSet` pivot_tvs) qtvs
- = fireTransRule "TrPushAxSym" co1 co2 $
- if sym2
- -- TrPushAxSym
- then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
- -- TrPushSymAx
- else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
where
co1_is_axiom_maybe = isAxiom_maybe co1
co2_is_axiom_maybe = isAxiom_maybe co2
=====================================
compiler/GHC/Core/Opt/Simplify/Env.hs
=====================================
@@ -23,7 +23,7 @@ module GHC.Core.Opt.Simplify.Env (
getInScope, setInScopeFromE, setInScopeFromF,
setInScopeSet, modifyInScope, addNewInScopeIds,
getSimplRules, enterRecGroupRHSs,
- bumpCallDepth, reSimplifying,
+ reSimplifying,
-- * Substitution results
SimplSR(..), mkContEx, substId, lookupRecBndr,
@@ -156,6 +156,17 @@ following table:
| Set by user | SimplMode | TopEnvConfig |
| Computed on initialization | SimplEnv | SimplTopEnv |
+Note [Inline depth]
+~~~~~~~~~~~~~~~~~~~
+When we inline an /already-simplified/ unfolding, we
+* Zap the substitution environment; the inlined thing is an OutExpr
+* Bump the seInlineDepth in the SimplEnv
+Both these tasks are done in zapSubstEnv.
+
+The seInlineDepth tells us how deep in inlining we are. Currently,
+seInlineDepth is used for just one purpose: when we encounter a
+coercion we don't apply optCoercion to it if seInlineDepth>0.
+Reason: it has already been optimised once, no point in doing so again.
-}
data SimplEnv
@@ -185,9 +196,11 @@ data SimplEnv
-- They are all OutVars, and all bound in this module
, seInScope :: !InScopeSet -- OutVars only
- , seCaseDepth :: !Int -- Depth of multi-branch case alternatives
- , seCallDepth :: !Int -- 0 initially, 1 when we inline an already-simplified
- -- unfolding, and simplify again; and so on
+ , seCaseDepth :: !Int -- Depth of multi-branch case alternatives
+
+ , seInlineDepth :: !Int -- 0 initially, 1 when we inline an already-simplified
+ -- unfolding, and simplify again; and so on
+ -- See Note [Inline depth]
}
seArityOpts :: SimplEnv -> ArityOpts
@@ -495,15 +508,15 @@ points we're substituting. -}
mkSimplEnv :: SimplMode -> (FamInstEnv, FamInstEnv) -> SimplEnv
mkSimplEnv mode fam_envs
- = SimplEnv { seMode = mode
- , seFamEnvs = fam_envs
- , seInScope = init_in_scope
- , seTvSubst = emptyVarEnv
- , seCvSubst = emptyVarEnv
- , seIdSubst = emptyVarEnv
- , seRecIds = emptyUnVarSet
- , seCaseDepth = 0
- , seCallDepth = 0 }
+ = SimplEnv { seMode = mode
+ , seFamEnvs = fam_envs
+ , seInScope = init_in_scope
+ , seTvSubst = emptyVarEnv
+ , seCvSubst = emptyVarEnv
+ , seIdSubst = emptyVarEnv
+ , seRecIds = emptyUnVarSet
+ , seCaseDepth = 0
+ , seInlineDepth = 0 }
-- The top level "enclosing CC" is "SUBSUMED".
init_in_scope :: InScopeSet
@@ -539,11 +552,8 @@ updMode upd env
bumpCaseDepth :: SimplEnv -> SimplEnv
bumpCaseDepth env = env { seCaseDepth = seCaseDepth env + 1 }
-bumpCallDepth :: SimplEnv -> SimplEnv
-bumpCallDepth env = env { seCallDepth = seCallDepth env + 1 }
-
reSimplifying :: SimplEnv -> Bool
-reSimplifying (SimplEnv { seCallDepth = n }) = n>0
+reSimplifying (SimplEnv { seInlineDepth = n }) = n>0
---------------------
extendIdSubst :: SimplEnv -> Id -> SimplSR -> SimplEnv
@@ -630,9 +640,12 @@ setInScopeFromE.
---------------------
zapSubstEnv :: SimplEnv -> SimplEnv
-zapSubstEnv env@(SimplEnv { seCallDepth = n })
+-- See Note [Inline depth]
+-- We call zapSubstEnv precisely when we are about to
+-- simplify an already-simplified term
+zapSubstEnv env@(SimplEnv { seInlineDepth = n })
= env { seTvSubst = emptyVarEnv, seCvSubst = emptyVarEnv, seIdSubst = emptyVarEnv
- , seCallDepth = n+1 }
+ , seInlineDepth = n+1 }
setSubstEnv :: SimplEnv -> TvSubstEnv -> CvSubstEnv -> SimplIdSubst -> SimplEnv
setSubstEnv env tvs cvs ids = env { seTvSubst = tvs, seCvSubst = cvs, seIdSubst = ids }
=====================================
compiler/GHC/Core/Opt/Simplify/Iteration.hs
=====================================
@@ -423,8 +423,7 @@ simplAuxBind _str env bndr new_rhs
-- have no NOLINE pragmas, nor RULEs
| exprIsTrivial new_rhs -- Short-cut for let x = y in ...
|| case (idOccInfo bndr) of
- OneOcc{ occ_n_br = 1, occ_in_lam = NotInsideLam } -> -- pprTrace ("simplAuxBind:"++_str) (ppr bndr <+> equals <+> ppr new_rhs) $
- True
+ OneOcc{ occ_n_br = 1, occ_in_lam = NotInsideLam } -> True
_ -> False
= return ( emptyFloats env
, case new_rhs of
@@ -1334,13 +1333,16 @@ simplCoercionF env co cont
simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion
simplCoercion env co
- = do { let opt_co | reSimplifying env
- = substCo env co
- | otherwise
- = optCoercion opts (getSubst env) co
+ = do { let opt_co | reSimplifying env = substCo env co
+ | otherwise = optCoercion opts subst co
+ -- If (reSimplifying env) is True we have already
+ -- simplified this coercion once, and we don't
+ -- want do so again; doing so repeatedly risks
+ -- non-linear behaviour
; seqCo opt_co `seq` return opt_co }
where
- opts = seOptCoercionOpts env
+ subst = getSubst env
+ opts = seOptCoercionOpts env
-----------------------------------
-- | Push a TickIt context outwards past applications and cases, as
@@ -1639,10 +1641,8 @@ simplCast env body co0 cont0
addCoerce :: OutCoercion -> Bool -> SimplCont -> SimplM SimplCont
addCoerce co1 _ (CastIt { sc_co = co2, sc_cont = cont }) -- See Note [Optimising reflexivity]
- | isReflCo co' = return cont
- | otherwise = addCoerce co' False cont
- where -- False: co' is not fully optimised
- co' = mkTransCo co1 co2
+ = addCoerce (mkTransCo co1 co2) False cont
+ -- False: (mkTransCo co1 co2) is not fully optimised
addCoerce co opt (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail })
| Just (arg_ty', m_co') <- pushCoTyArg co arg_ty
@@ -1661,6 +1661,9 @@ simplCast env body co0 cont0
addCoerce co opt cont@(ApplyToVal { sc_arg = arg, sc_env = arg_se
, sc_dup = dup, sc_cont = tail
, sc_hole_ty = fun_ty })
+ | not opt -- pushCoValArg duplicates the coercion, so optimise first
+ = addCoerce (optOutCoercion env co opt) True cont
+
| Just (m_co1, m_co2) <- pushCoValArg co
, fixed_rep m_co1
= {-#SCC "addCoerce-pushCoValArg" #-}
@@ -1685,10 +1688,10 @@ simplCast env body co0 cont0
, sc_hole_ty = coercionLKind co }) } } }
addCoerce co opt cont
- | isReflexiveCo co = return cont -- Having this at the end makes a huge
- -- difference in T12227, for some reason
- -- See Note [Optimising reflexivity]
- | otherwise = return (CastIt { sc_co = co, sc_opt = opt, sc_cont = cont })
+ | isReflCo co = return cont -- Having this at the end makes a huge
+ -- difference in T12227, for some reason
+ -- See Note [Optimising reflexivity]
+ | otherwise = return (CastIt { sc_co = co, sc_opt = opt, sc_cont = cont })
fixed_rep :: MCoercionR -> Bool
fixed_rep MRefl = True
@@ -3901,6 +3904,7 @@ mkDupableAlt env case_bndr jfloats (Alt con alt_bndrs alt_rhs_in)
-- See Note [Duplicated env]
ok_to_dup_alt :: OutId -> [OutVar] -> OutExpr -> Bool
+-- See Note [Duplicating alternatives]
ok_to_dup_alt case_bndr alt_bndrs alt_rhs
| (Var v, args) <- collectArgs alt_rhs
, all exprIsTrivial args
@@ -3913,6 +3917,27 @@ ok_to_dup_alt case_bndr alt_bndrs alt_rhs
bndr_set = mkVarSet (case_bndr : alt_bndrs)
{-
+Note [Duplicating alternatives]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When should we duplicate an alternative, and when should we make a join point?
+We don't want to make a join point if it will /definitely/ be inlined; that
+takes extra work to build, and an extra Simplifier iteration to do the inlining.
+So consider
+
+ case (case x of True -> e2; False -> e2) of
+ K1 a b -> f b a
+ K2 x -> g x v
+ K3 v -> Just v
+
+The (f b a) would turn into a join point like
+ $j1 a b = f b a
+which would immediately inline again because the call is not smaller than the RHS.
+On the other hand, the (g x v) turns into
+ $j2 x = g x v
+which won't imediately inline. Finally the (Just v) would turn into
+ $j3 v = Just v
+and you might think that would immediately inline.
+
Note [Fusing case continuations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's important to fuse two successive case continuations when the
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -152,7 +152,7 @@ data Type
-- for example unsaturated type synonyms
-- can appear as the right hand side of a type synonym.
- | ForAllTy
+ | ForAllTy -- See Note [Weird typing rule for ForAllTy]
{-# UNPACK #-} !ForAllTyBinder
Type -- ^ A Π type.
-- Note [When we quantify over a coercion variable]
@@ -1173,11 +1173,11 @@ because the kinds of the bound tyvars can be different.
The typing rule is:
- kind_co : k1 ~ k2
- tv1:k1 |- co : t1 ~ t2
+ kind_co : k1 ~N k2
+ tv1:k1 |- co : t1 ~r t2
-------------------------------------------------------------------
- ForAllCo tv1 kind_co co : all tv1:k1. t1 ~
- all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
+ ForAllCo tv1 kind_co co : all tv1:k1. t1 ~r
+ all tv1:k2. (t2[tv1 := (tv1 |> sym kind_co)])
First, the TyCoVar stored in a ForAllCo is really an optimisation: this field
should be a Name, as its kind is redundant. Thinking of the field as a Name
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -1875,8 +1875,8 @@ ppr_co _ (IfaceUnivCo prov role ty1 ty2)
ppr_co ctxt_prec (IfaceInstCo co ty)
= maybeParen ctxt_prec appPrec $
- text "Inst" <+> pprParendIfaceCoercion co
- <+> pprParendIfaceCoercion ty
+ text "Inst" <+> sep [ pprParendIfaceCoercion co
+ , pprParendIfaceCoercion ty ]
ppr_co ctxt_prec (IfaceAxiomRuleCo tc cos)
= maybeParen ctxt_prec appPrec $ ppr tc <+> parens (interpp'SP cos)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/8efcee737e8dfb7287a5ef9cdca0590a80b70750...99d011f850d8d5bc408e2e7abfb955554f869738
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/8efcee737e8dfb7287a5ef9cdca0590a80b70750...99d011f850d8d5bc408e2e7abfb955554f869738
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/20230705/a357c888/attachment-0001.html>
More information about the ghc-commits
mailing list