Commit 55a3f855 authored by Ningning Xie's avatar Ningning Xie Committed by Richard Eisenberg

Refactor coercion rule

Summary:
The patch is an attempt on #15192.

It defines a new coercion rule

```
 | GRefl Role Type MCoercion
```

which correspondes to the typing rule

```
     t1 : k1
  ------------------------------------
  GRefl r t1 MRefl: t1 ~r t1

     t1 : k1       co :: k1 ~ k2
  ------------------------------------
  GRefl r t1 (MCo co) : t1 ~r t1 |> co
```

MCoercion wraps a coercion, which might be reflexive (MRefl)
or not (MCo co). To know more about MCoercion see #14975.

We keep Refl ty as a special case for nominal reflexive coercions,
naemly, Refl ty :: ty ~n ty.

This commit is meant to be a general performance improvement,
but there are a few regressions. See #15192, comment:13 for
more information.

Test Plan: ./validate

Reviewers: bgamari, goldfire, simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15192

Differential Revision: https://phabricator.haskell.org/D4747
parent 6595bee7
......@@ -641,8 +641,14 @@ rnIfaceLetBndr (IfLetBndr fs ty info jpi)
rnIfaceLamBndr :: Rename IfaceLamBndr
rnIfaceLamBndr (bndr, oneshot) = (,) <$> rnIfaceBndr bndr <*> pure oneshot
rnIfaceMCo :: Rename IfaceMCoercion
rnIfaceMCo IfaceMRefl = pure IfaceMRefl
rnIfaceMCo (IfaceMCo co) = IfaceMCo <$> rnIfaceCo co
rnIfaceCo :: Rename IfaceCoercion
rnIfaceCo (IfaceReflCo role ty) = IfaceReflCo role <$> rnIfaceType ty
rnIfaceCo (IfaceReflCo ty) = IfaceReflCo <$> rnIfaceType ty
rnIfaceCo (IfaceGReflCo role ty mco)
= IfaceGReflCo role <$> rnIfaceType ty <*> rnIfaceMCo mco
rnIfaceCo (IfaceFunCo role co1 co2)
= IfaceFunCo role <$> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceTyConAppCo role tc cos)
......@@ -670,7 +676,6 @@ rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c
rnIfaceCo (IfaceAxiomRuleCo ax cos)
= IfaceAxiomRuleCo ax <$> mapM rnIfaceCo cos
rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c
rnIfaceCo (IfaceCoherenceCo c1 c2) = IfaceCoherenceCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
rnIfaceTyCon :: Rename IfaceTyCon
rnIfaceTyCon (IfaceTyCon n info)
......
......@@ -366,8 +366,13 @@ orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet
orphNamesOfTypes :: [Type] -> NameSet
orphNamesOfTypes = orphNamesOfThings orphNamesOfType
orphNamesOfMCo :: MCoercion -> NameSet
orphNamesOfMCo MRefl = emptyNameSet
orphNamesOfMCo (MCo co) = orphNamesOfCo co
orphNamesOfCo :: Coercion -> NameSet
orphNamesOfCo (Refl _ ty) = orphNamesOfType ty
orphNamesOfCo (Refl ty) = orphNamesOfType ty
orphNamesOfCo (GRefl _ ty mco) = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
orphNamesOfCo (ForAllCo _ kind_co co)
......@@ -381,7 +386,6 @@ orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNames
orphNamesOfCo (NthCo _ _ co) = orphNamesOfCo co
orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg
orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
orphNamesOfCo (KindCo co) = orphNamesOfCo co
orphNamesOfCo (SubCo co) = orphNamesOfCo co
orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs
......
......@@ -1617,15 +1617,28 @@ lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, Linted
--
-- If lintCoercion co = (k1, k2, s1, s2, r)
-- then co :: s1 ~r s2
-- s1 :: k2
-- s1 :: k1
-- s2 :: k2
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoercion (Refl r ty)
lintCoercion (Refl ty)
= do { k <- lintType ty
; return (k, k, ty, ty, Nominal) }
lintCoercion (GRefl r ty MRefl)
= do { k <- lintType ty
; return (k, k, ty, ty, r) }
lintCoercion (GRefl r ty (MCo co))
= do { k <- lintType ty
; (_, _, k1, k2, r') <- lintCoercion co
; ensureEqTys k k1
(hang (text "GRefl coercion kind mis-match:" <+> ppr co)
2 (vcat [ppr ty, ppr k, ppr k1]))
; lintRole co Nominal r'
; return (k1, k2, ty, mkCastTy ty co, r) }
lintCoercion co@(TyConAppCo r tc cos)
| tc `hasKey` funTyConKey
, [_rep1,_rep2,_co1,_co2] <- cos
......@@ -1646,7 +1659,7 @@ lintCoercion co@(TyConAppCo r tc cos)
lintCoercion co@(AppCo co1 co2)
| TyConAppCo {} <- co1
= failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
| Refl _ (TyConApp {}) <- co1
| Just (TyConApp {}, _) <- isReflCo_maybe co1
= failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
| otherwise
= do { (k1, k2, s1, s2, r1) <- lintCoercion co1
......@@ -1884,12 +1897,6 @@ lintCoercion co@(AxiomInstCo con ind cos)
; return (extendTCvSubst subst_l ktv s',
extendTCvSubst subst_r ktv t') }
lintCoercion (CoherenceCo co1 co2)
= do { (_, k2, t1, t2, r) <- lintCoercion co1
; let lhsty = mkCastTy t1 co2
; k1' <- lintType lhsty
; return (k1', k2, lhsty, t2, r) }
lintCoercion (KindCo co)
= do { (k1, k2, _, _, _) <- lintCoercion co
; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
......
......@@ -995,7 +995,7 @@ pushCoTyArg co ty
-- kinds of the types related by a coercion between forall-types.
-- See the NthCo case in CoreLint.
co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1)
co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1)
-- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
-- Arg of mkInstCo is always nominal, hence mkNomReflCo
......
......@@ -1425,8 +1425,14 @@ freeNamesIfType (IfaceDFunTy s t) = freeNamesIfType s &&& freeNamesIfType t
freeNamesIfType (IfaceCastTy t c) = freeNamesIfType t &&& freeNamesIfCoercion c
freeNamesIfType (IfaceCoercionTy c) = freeNamesIfCoercion c
freeNamesIfMCoercion :: IfaceMCoercion -> NameSet
freeNamesIfMCoercion IfaceMRefl = emptyNameSet
freeNamesIfMCoercion (IfaceMCo co) = freeNamesIfCoercion co
freeNamesIfCoercion :: IfaceCoercion -> NameSet
freeNamesIfCoercion (IfaceReflCo _ t) = freeNamesIfType t
freeNamesIfCoercion (IfaceReflCo t) = freeNamesIfType t
freeNamesIfCoercion (IfaceGReflCo _ t mco)
= freeNamesIfType t &&& freeNamesIfMCoercion mco
freeNamesIfCoercion (IfaceFunCo _ c1 c2)
= freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
freeNamesIfCoercion (IfaceTyConAppCo _ tc cos)
......@@ -1452,8 +1458,6 @@ freeNamesIfCoercion (IfaceLRCo _ co)
= freeNamesIfCoercion co
freeNamesIfCoercion (IfaceInstCo co co2)
= freeNamesIfCoercion co &&& freeNamesIfCoercion co2
freeNamesIfCoercion (IfaceCoherenceCo c1 c2)
= freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
freeNamesIfCoercion (IfaceKindCo c)
= freeNamesIfCoercion c
freeNamesIfCoercion (IfaceSubCo co)
......
......@@ -14,6 +14,7 @@ module IfaceType (
IfExtName, IfLclName,
IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
IfaceMCoercion(..),
IfaceUnivCoProv(..),
IfaceTyCon(..), IfaceTyConInfo(..), IfaceTyConSort(..), IsPromoted(..),
IfaceTyLit(..), IfaceTcArgs(..),
......@@ -280,8 +281,13 @@ data IfaceTyConInfo -- Used to guide pretty-printing
, ifaceTyConSort :: IfaceTyConSort }
deriving (Eq)
data IfaceMCoercion
= IfaceMRefl
| IfaceMCo IfaceCoercion
data IfaceCoercion
= IfaceReflCo Role IfaceType
= IfaceReflCo IfaceType
| IfaceGReflCo Role IfaceType (IfaceMCoercion)
| IfaceFunCo Role IfaceCoercion IfaceCoercion
| IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
| IfaceAppCo IfaceCoercion IfaceCoercion
......@@ -298,7 +304,6 @@ data IfaceCoercion
| IfaceNthCo Int IfaceCoercion
| IfaceLRCo LeftOrRight IfaceCoercion
| IfaceInstCo IfaceCoercion IfaceCoercion
| IfaceCoherenceCo IfaceCoercion IfaceCoercion
| IfaceKindCo IfaceCoercion
| IfaceSubCo IfaceCoercion
| IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
......@@ -457,8 +462,12 @@ substIfaceType env ty
go (IfaceCastTy ty co) = IfaceCastTy (go ty) (go_co co)
go (IfaceCoercionTy co) = IfaceCoercionTy (go_co co)
go_co (IfaceReflCo r ty) = IfaceReflCo r (go ty)
go_co (IfaceFunCo r c1 c2) = IfaceFunCo r (go_co c1) (go_co c2)
go_mco IfaceMRefl = IfaceMRefl
go_mco (IfaceMCo co) = IfaceMCo $ go_co co
go_co (IfaceReflCo ty) = IfaceReflCo (go ty)
go_co (IfaceGReflCo r ty mco) = IfaceGReflCo r (go ty) (go_mco mco)
go_co (IfaceFunCo r c1 c2) = IfaceFunCo r (go_co c1) (go_co c2)
go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
go_co (IfaceAppCo c1 c2) = IfaceAppCo (go_co c1) (go_co c2)
go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty)
......@@ -472,7 +481,6 @@ substIfaceType env ty
go_co (IfaceNthCo n co) = IfaceNthCo n (go_co co)
go_co (IfaceLRCo lr co) = IfaceLRCo lr (go_co co)
go_co (IfaceInstCo c1 c2) = IfaceInstCo (go_co c1) (go_co c2)
go_co (IfaceCoherenceCo c1 c2) = IfaceCoherenceCo (go_co c1) (go_co c2)
go_co (IfaceKindCo co) = IfaceKindCo (go_co co)
go_co (IfaceSubCo co) = IfaceSubCo (go_co co)
go_co (IfaceAxiomRuleCo n cos) = IfaceAxiomRuleCo n (go_cos cos)
......@@ -1197,7 +1205,12 @@ pprIfaceCoercion = ppr_co topPrec
pprParendIfaceCoercion = ppr_co appPrec
ppr_co :: PprPrec -> IfaceCoercion -> SDoc
ppr_co _ (IfaceReflCo r ty) = angleBrackets (ppr ty) <> ppr_role r
ppr_co _ (IfaceReflCo ty) = angleBrackets (ppr ty) <> ppr_role Nominal
ppr_co _ (IfaceGReflCo r ty IfaceMRefl)
= angleBrackets (ppr ty) <> ppr_role r
ppr_co ctxt_prec (IfaceGReflCo r ty (IfaceMCo co))
= ppr_special_co ctxt_prec
(text "GRefl" <+> ppr r <+> pprParendIfaceType ty) [co]
ppr_co ctxt_prec (IfaceFunCo r co1 co2)
= maybeParen ctxt_prec funPrec $
sep (ppr_co funPrec co1 : ppr_fun_tail co2)
......@@ -1258,8 +1271,6 @@ ppr_co ctxt_prec (IfaceLRCo lr co)
= ppr_special_co ctxt_prec (ppr lr) [co]
ppr_co ctxt_prec (IfaceSubCo co)
= ppr_special_co ctxt_prec (text "Sub") [co]
ppr_co ctxt_prec (IfaceCoherenceCo co1 co2)
= ppr_special_co ctxt_prec (text "Coh") [co1,co2]
ppr_co ctxt_prec (IfaceKindCo co)
= ppr_special_co ctxt_prec (text "Kind") [co]
......@@ -1490,64 +1501,79 @@ instance Binary IfaceType where
_ -> do n <- get bh
return (IfaceLitTy n)
instance Binary IfaceMCoercion where
put_ bh IfaceMRefl = do
putByte bh 1
put_ bh (IfaceMCo co) = do
putByte bh 2
put_ bh co
get bh = do
tag <- getByte bh
case tag of
1 -> return IfaceMRefl
2 -> do a <- get bh
return $ IfaceMCo a
_ -> panic ("get IfaceMCoercion " ++ show tag)
instance Binary IfaceCoercion where
put_ bh (IfaceReflCo a b) = do
put_ bh (IfaceReflCo a) = do
putByte bh 1
put_ bh a
put_ bh (IfaceGReflCo a b c) = do
putByte bh 2
put_ bh a
put_ bh b
put_ bh c
put_ bh (IfaceFunCo a b c) = do
putByte bh 2
putByte bh 3
put_ bh a
put_ bh b
put_ bh c
put_ bh (IfaceTyConAppCo a b c) = do
putByte bh 3
putByte bh 4
put_ bh a
put_ bh b
put_ bh c
put_ bh (IfaceAppCo a b) = do
putByte bh 4
putByte bh 5
put_ bh a
put_ bh b
put_ bh (IfaceForAllCo a b c) = do
putByte bh 5
putByte bh 6
put_ bh a
put_ bh b
put_ bh c
put_ bh (IfaceCoVarCo a) = do
putByte bh 6
putByte bh 7
put_ bh a
put_ bh (IfaceAxiomInstCo a b c) = do
putByte bh 7
putByte bh 8
put_ bh a
put_ bh b
put_ bh c
put_ bh (IfaceUnivCo a b c d) = do
putByte bh 8
putByte bh 9
put_ bh a
put_ bh b
put_ bh c
put_ bh d
put_ bh (IfaceSymCo a) = do
putByte bh 9
put_ bh a
put_ bh (IfaceTransCo a b) = do
putByte bh 10
put_ bh a
put_ bh b
put_ bh (IfaceNthCo a b) = do
put_ bh (IfaceTransCo a b) = do
putByte bh 11
put_ bh a
put_ bh b
put_ bh (IfaceLRCo a b) = do
put_ bh (IfaceNthCo a b) = do
putByte bh 12
put_ bh a
put_ bh b
put_ bh (IfaceInstCo a b) = do
put_ bh (IfaceLRCo a b) = do
putByte bh 13
put_ bh a
put_ bh b
put_ bh (IfaceCoherenceCo a b) = do
put_ bh (IfaceInstCo a b) = do
putByte bh 14
put_ bh a
put_ bh b
......@@ -1571,51 +1597,51 @@ instance Binary IfaceCoercion where
tag <- getByte bh
case tag of
1 -> do a <- get bh
b <- get bh
return $ IfaceReflCo a b
return $ IfaceReflCo a
2 -> do a <- get bh
b <- get bh
c <- get bh
return $ IfaceFunCo a b c
return $ IfaceGReflCo a b c
3 -> do a <- get bh
b <- get bh
c <- get bh
return $ IfaceTyConAppCo a b c
return $ IfaceFunCo a b c
4 -> do a <- get bh
b <- get bh
return $ IfaceAppCo a b
c <- get bh
return $ IfaceTyConAppCo a b c
5 -> do a <- get bh
b <- get bh
return $ IfaceAppCo a b
6 -> do a <- get bh
b <- get bh
c <- get bh
return $ IfaceForAllCo a b c
6 -> do a <- get bh
return $ IfaceCoVarCo a
7 -> do a <- get bh
return $ IfaceCoVarCo a
8 -> do a <- get bh
b <- get bh
c <- get bh
return $ IfaceAxiomInstCo a b c
8 -> do a <- get bh
9 -> do a <- get bh
b <- get bh
c <- get bh
d <- get bh
return $ IfaceUnivCo a b c d
9 -> do a <- get bh
return $ IfaceSymCo a
10-> do a <- get bh
b <- get bh
return $ IfaceTransCo a b
return $ IfaceSymCo a
11-> do a <- get bh
b <- get bh
return $ IfaceNthCo a b
return $ IfaceTransCo a b
12-> do a <- get bh
b <- get bh
return $ IfaceLRCo a b
return $ IfaceNthCo a b
13-> do a <- get bh
b <- get bh
return $ IfaceInstCo a b
return $ IfaceLRCo a b
14-> do a <- get bh
b <- get bh
return $ IfaceCoherenceCo a b
return $ IfaceInstCo a b
15-> do a <- get bh
return $ IfaceKindCo a
16-> do a <- get bh
......
......@@ -1199,7 +1199,11 @@ tcIfaceTyLit (IfaceStrTyLit n) = return (StrTyLit n)
tcIfaceCo :: IfaceCoercion -> IfL Coercion
tcIfaceCo = go
where
go (IfaceReflCo r t) = Refl r <$> tcIfaceType t
go_mco IfaceMRefl = pure MRefl
go_mco (IfaceMCo co) = MCo <$> (go co)
go (IfaceReflCo t) = Refl <$> tcIfaceType t
go (IfaceGReflCo r t mco) = GRefl r <$> tcIfaceType t <*> go_mco mco
go (IfaceFunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
go (IfaceTyConAppCo r tc cs)
= TyConAppCo r <$> tcIfaceTyCon tc <*> mapM go cs
......@@ -1219,8 +1223,6 @@ tcIfaceCo = go
go (IfaceNthCo d c) = do { c' <- go c
; return $ mkNthCo (nthCoRole d c') d c' }
go (IfaceLRCo lr c) = LRCo lr <$> go c
go (IfaceCoherenceCo c1 c2) = CoherenceCo <$> go c1
<*> go c2
go (IfaceKindCo c) = KindCo <$> go c
go (IfaceSubCo c) = SubCo <$> go c
go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> tcIfaceCoAxiomRule ax
......
......@@ -221,7 +221,11 @@ toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
toIfaceCoercionX fr co
= go co
where
go (Refl r ty) = IfaceReflCo r (toIfaceTypeX fr ty)
go_mco MRefl = IfaceMRefl
go_mco (MCo co) = IfaceMCo $ go co
go (Refl ty) = IfaceReflCo (toIfaceTypeX fr ty)
go (GRefl r ty mco) = IfaceGReflCo r (toIfaceTypeX fr ty) (go_mco mco)
go (CoVarCo cv)
-- See [TcTyVars in IfaceType] in IfaceType
| cv `elemVarSet` fr = IfaceFreeCoVar cv
......@@ -234,7 +238,6 @@ toIfaceCoercionX fr co
go (NthCo _r d co) = IfaceNthCo d (go co)
go (LRCo lr co) = IfaceLRCo lr (go co)
go (InstCo co arg) = IfaceInstCo (go co) (go arg)
go (CoherenceCo c1 c2) = IfaceCoherenceCo (go c1) (go c2)
go (KindCo c) = IfaceKindCo (go c)
go (SubCo co) = IfaceSubCo (go co)
go (AxiomRuleCo co cs) = IfaceAxiomRuleCo (coaxrName co) (map go cs)
......
......@@ -1291,7 +1291,7 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
, ppr ty1 <+> text "|>" <+> ppr co1
, ppr ps_ty2 ])
; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
(mkTcReflCo role ty1 `mkTcCoherenceRightCo` co1)
(mkTcGReflRightCo role ty1 co1)
(mkTcReflCo role ps_ty2)
; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
where
......@@ -1737,7 +1737,10 @@ canCFunEqCan ev fn tys fsk
-- new_co :: F tys' ~ new_fsk
-- co :: F tys ~ (new_fsk |> kind_co)
co = mkTcSymCo lhs_co `mkTcTransCo`
(new_co `mkTcCoherenceRightCo` kind_co)
mkTcCoherenceRightCo Nominal
(mkTyVarTy new_fsk)
kind_co
new_co
; traceTcS "Discharging fmv/fsk due to hetero flattening" (ppr ev)
; dischargeFunEq ev fsk co xi
......@@ -1788,7 +1791,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
new_rhs = xi2 `mkCastTy` rhs_kind_co
ps_rhs = ps_xi2 `mkCastTy` rhs_kind_co
rhs_co = mkTcReflCo role xi2 `mkTcCoherenceLeftCo` rhs_kind_co
rhs_co = mkTcGReflLeftCo role xi2 rhs_kind_co
; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs
(mkTcReflCo role xi1) rhs_co
......@@ -1803,8 +1806,8 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
new_rhs = xi2 `mkCastTy` sym_k2_co -- :: flat_k2
ps_rhs = ps_xi2 `mkCastTy` sym_k2_co
lhs_co = mkReflCo role xi1 `mkTcCoherenceLeftCo` sym_k1_co
rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` sym_k2_co
lhs_co = mkTcGReflLeftCo role xi1 sym_k1_co
rhs_co = mkTcGReflLeftCo role xi2 sym_k2_co
-- lhs_co :: (xi1 |> sym k1_co) ~ xi1
-- rhs_co :: (xi2 |> sym k2_co) ~ xi2
......@@ -1841,11 +1844,11 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1
rhs' = mkCastTy xi2 homo_co -- :: kind(tv1)
ps_rhs' = mkCastTy ps_xi2 homo_co -- :: kind(tv1)
rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co
rhs_co = mkTcGReflLeftCo role xi2 homo_co
-- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2
lhs' = mkTyVarTy tv1 -- :: kind(tv1)
lhs_co = mkReflCo role lhs' `mkTcCoherenceRightCo` co1
lhs_co = mkTcGReflRightCo role lhs' co1
-- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
; traceTcS "Hetero equality gives rise to given kind equality"
......@@ -1895,10 +1898,10 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
sym_co2 = mkTcSymCo co2
ty1 = mkTyVarTy tv1
new_lhs = ty1 `mkCastTy` sym_co2
lhs_co = mkReflCo role ty1 `mkTcCoherenceLeftCo` sym_co2
lhs_co = mkTcGReflLeftCo role ty1 sym_co2
new_rhs = mkTyVarTy tv2
rhs_co = mkReflCo role new_rhs `mkTcCoherenceRightCo` co2
rhs_co = mkTcGReflRightCo role new_rhs co2
; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
......
......@@ -35,7 +35,9 @@ module TcEvidence (
mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
tcDowngradeRole,
mkTcAxiomRuleCo, mkTcCoherenceLeftCo, mkTcCoherenceRightCo, mkTcPhantomCo,
mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflLeftCo, mkTcPhantomCo,
mkTcCoherenceLeftCo,
mkTcCoherenceRightCo,
mkTcKindCo,
tcCoercionKind, coVarsOfTcCo,
mkTcCoVarCo,
......@@ -115,8 +117,12 @@ mkTcSubCo :: TcCoercionN -> TcCoercionR
maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion
mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion
mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcGReflLeftCo :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcCoherenceLeftCo :: Role -> TcType -> TcCoercionN
-> TcCoercion -> TcCoercion
mkTcCoherenceRightCo :: Role -> TcType -> TcCoercionN
-> TcCoercion -> TcCoercion
mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP
mkTcKindCo :: TcCoercion -> TcCoercionN
mkTcCoVarCo :: CoVar -> TcCoercion
......@@ -148,6 +154,8 @@ mkTcSubCo = mkSubCo
maybeTcSubCo = maybeSubCo
tcDowngradeRole = downgradeRole
mkTcAxiomRuleCo = mkAxiomRuleCo
mkTcGReflRightCo = mkGReflRightCo
mkTcGReflLeftCo = mkGReflLeftCo
mkTcCoherenceLeftCo = mkCoherenceLeftCo
mkTcCoherenceRightCo = mkCoherenceRightCo
mkTcPhantomCo = mkPhantomCo
......
......@@ -1115,6 +1115,17 @@ as desired. (Why do we want Star? Because we started with something of kind Star
Whew.
Note [flatten_exact_fam_app_fully performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The refactor of GRefl seems to cause performance trouble for T9872x: the allocation of flatten_exact_fam_app_fully_performance increased. See note [Generalized reflexive coercion] in TyCoRep for more information about GRefl and Trac #15192 for the current state.
The explicit pattern match in homogenise_result helps with T9872a, b, c.
Still, it increases the expected allocation of T9872d by ~2%.
TODO: a step-by-step replay of the refactor to analyze the performance.
-}
{-# INLINE flatten_args_tc #-}
......@@ -1208,12 +1219,12 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
--
-- let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder)
-- casted_xi = xi `mkCastTy` kind_co
-- casted_co = co `mkTcCoherenceLeftCo` kind_co
-- casted_co = xi |> kind_co ~r xi ; co
--
-- but this isn't necessary:
-- mkTcSymCo (Refl a b) = Refl a b,
-- mkCastTy x (Refl _ _) = x
-- mkTcCoherenceLeftCo x (Refl _ _) = x
-- mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
--
-- Also, no need to check isAnonTyBinder or isNamedTyBinder, since
-- we've already established that they're all anonymous.
......@@ -1229,7 +1240,7 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
finish (xis, cos, binders) = (xis, cos, kind_co)
where
final_kind = mkPiTys binders orig_inner_ki
kind_co = mkReflCo Nominal final_kind
kind_co = mkNomReflCo final_kind
{-# INLINE flatten_args_slow #-}
-- | Slow path, compared to flatten_args_fast, because this one must track
......@@ -1283,7 +1294,7 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
; let kind_co = mkTcSymCo $
liftCoSubst Nominal lc (tyBinderType binder)
!casted_xi = xi `mkCastTy` kind_co
casted_co = co `mkTcCoherenceLeftCo` kind_co
casted_co = mkTcCoherenceLeftCo role xi kind_co co
-- now, extend the lifting context with the new binding
!new_lc | Just tv <- tyBinderVar_maybe binder
......@@ -1314,13 +1325,13 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
<- go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_tys
-- cos_out :: xis_out ~ casted_tys
-- we need to return cos :: xis_out ~ tys
--
-- zipWith has the map first because it will fuse.
; let cos = zipWith (flip mkTcCoherenceRightCo)
(map mkTcSymCo arg_cos)
cos_out
; let cos = zipWith3 mkTcGReflRightCo
roles
casted_tys
(map mkTcSymCo arg_cos)
cos' = zipWith mkTransCo cos_out cos
; return (xis_out, cos, res_co_out `mkTcTransCo` res_co) }
; return (xis_out, cos', res_co_out `mkTcTransCo` res_co) }
go _ _ _ _ _ _ _ = pprPanic
"flatten_args wandered into deeper water than usual" (vcat [])
......@@ -1408,7 +1419,8 @@ flatten_one (CastTy ty g)
= do { (xi, co) <- flatten_one ty
; (g', _) <- flatten_co g
; return (mkCastTy xi g', castCoercionKind co g' g) }
; role <- getRole
; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }
flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
......@@ -1471,7 +1483,8 @@ flatten_app_ty_args fun_xi fun_co arg_tys
arg_co = mkAppCos fun_co arg_cos
; return (arg_xi, arg_co, kind_co) }
; return (homogenise_result xi co kind_co) }
; role <- getRole
; return (homogenise_result xi co role kind_co) }
flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
flatten_ty_con_app tc tys
......@@ -1479,18 +1492,21 @@ flatten_ty_con_app tc tys
; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys
; let tyconapp_xi = mkTyConApp tc xis
tyconapp_co = mkTyConAppCo role tc cos
; return (homogenise_result tyconapp_xi tyconapp_co kind_co) }
; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
-- Make the result of flattening homogeneous (Note [Flattening] (F2))
homogenise_result :: Xi -- a flattened type
-> Coercion -- :: xi ~ original ty