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/backpack/RnModIface.hs | |
| 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/backpack/RnModIface.hs')
| -rw-r--r-- | compiler/backpack/RnModIface.hs | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs index f807b39ce8..6b958df760 100644 --- a/compiler/backpack/RnModIface.hs +++ b/compiler/backpack/RnModIface.hs @@ -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) |