diff options
author | ningning <xnningxie@gmail.com> | 2018-07-09 20:02:03 -0400 |
---|---|---|
committer | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-07-09 21:35:31 -0400 |
commit | 55a3f8552c9dc9b84e204ec6623c698912795347 (patch) | |
tree | 3433832e7bc586c46cccd6204ce92748bc9b4a01 /compiler/iface | |
parent | 6595bee749ddb49d9058ed47ab7c1b6e7558ae17 (diff) | |
download | haskell-55a3f8552c9dc9b84e204ec6623c698912795347.tar.gz |
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
Diffstat (limited to 'compiler/iface')
-rw-r--r-- | compiler/iface/IfaceSyn.hs | 10 | ||||
-rw-r--r-- | compiler/iface/IfaceType.hs | 106 | ||||
-rw-r--r-- | compiler/iface/TcIface.hs | 8 | ||||
-rw-r--r-- | compiler/iface/ToIface.hs | 7 |
4 files changed, 83 insertions, 48 deletions
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index 778e8d637d..4a2d228bef 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -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) diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index 5a7f761d32..e3866f5e6d 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -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 diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index bffda71f0a..58bcd8c281 100644 --- a/compiler/iface/TcIface.hs +++ b/compiler/iface/TcIface.hs @@ -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 diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs index 4b810fa687..291aea36a7 100644 --- a/compiler/iface/ToIface.hs +++ b/compiler/iface/ToIface.hs @@ -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) |