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/coreSyn/CoreOpt.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/coreSyn/CoreOpt.hs')
| -rw-r--r-- | compiler/coreSyn/CoreOpt.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs index 0353ab6a75..8684c84515 100644 --- a/compiler/coreSyn/CoreOpt.hs +++ b/compiler/coreSyn/CoreOpt.hs @@ -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 |