diff options
| author | ningning <xnningxie@gmail.com> | 2018-09-15 10:16:47 -0400 |
|---|---|---|
| committer | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-09-15 10:28:41 -0400 |
| commit | ea5ade34788f29f5902c5475e94fbac13110eea5 (patch) | |
| tree | 3a17314dc67df885c3cdf681a6aec449ae808d8f /compiler/coreSyn/CoreMap.hs | |
| parent | c23f057f1753634e2bc0612969470efea6443031 (diff) | |
| download | haskell-ea5ade34788f29f5902c5475e94fbac13110eea5.tar.gz | |
Coercion Quantification
This patch corresponds to #15497.
According to https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2,
we would like to have coercion quantifications back. This will
allow us to migrate (~#) to be homogeneous, instead of its current
heterogeneous definition. This patch is (lots of) plumbing only. There
should be no user-visible effects.
An overview of changes:
- Both `ForAllTy` and `ForAllCo` can quantify over coercion variables,
but only in *Core*. All relevant functions are updated accordingly.
- Small changes that should be irrelevant to the main task:
1. removed dead code `mkTransAppCo` in Coercion
2. removed out-dated Note Computing a coercion kind and
roles in Coercion
3. Added `Eq4` in Note Respecting definitional equality in
TyCoRep, and updated `mkCastTy` accordingly.
4. Various updates and corrections of notes and typos.
- Haddock submodule needs to be changed too.
Acknowledgments:
This work was completed mostly during Ningning Xie's Google Summer
of Code, sponsored by Google. It was advised by Richard Eisenberg,
supported by NSF grant 1704041.
Test Plan: ./validate
Reviewers: goldfire, simonpj, bgamari, hvr, erikd, simonmar
Subscribers: RyanGlScott, monoidal, rwbarton, carter
GHC Trac Issues: #15497
Differential Revision: https://phabricator.haskell.org/D5054
Diffstat (limited to 'compiler/coreSyn/CoreMap.hs')
| -rw-r--r-- | compiler/coreSyn/CoreMap.hs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/compiler/coreSyn/CoreMap.hs b/compiler/coreSyn/CoreMap.hs index 0c9faa3efe..11f2fb1b11 100644 --- a/compiler/coreSyn/CoreMap.hs +++ b/compiler/coreSyn/CoreMap.hs @@ -522,8 +522,8 @@ instance Eq (DeBruijn Type) where -> tc == tc' && D env tys == D env' tys' (LitTy l, LitTy l') -> l == l' - (ForAllTy (TvBndr tv _) ty, ForAllTy (TvBndr tv' _) ty') - -> D env (tyVarKind tv) == D env' (tyVarKind tv') && + (ForAllTy (Bndr tv _) ty, ForAllTy (Bndr tv' _) ty') + -> D env (varType tv) == D env' (varType tv') && D (extendCME env tv) ty == D (extendCME env' tv') ty' (CoercionTy {}, CoercionTy {}) -> True @@ -563,7 +563,7 @@ lkT (D env ty) m = go ty m go (TyConApp tc []) = tm_tycon >.> lkDNamed tc go ty@(TyConApp _ (_:_)) = pprPanic "lkT TyConApp" (ppr ty) go (LitTy l) = tm_tylit >.> lkTyLit l - go (ForAllTy (TvBndr tv _) ty) = tm_forall >.> lkG (D (extendCME env tv) ty) + go (ForAllTy (Bndr tv _) ty) = tm_forall >.> lkG (D (extendCME env tv) ty) >=> lkBndr env tv go ty@(FunTy {}) = pprPanic "lkT FunTy" (ppr ty) go (CastTy t _) = go t @@ -580,7 +580,7 @@ xtT (D _ (TyConApp tc [])) f m = m { tm_tycon = tm_tycon m |> xtDNamed tc f xtT (D _ (LitTy l)) f m = m { tm_tylit = tm_tylit m |> xtTyLit l f } xtT (D env (CastTy t _)) f m = xtT (D env t) f m xtT (D _ (CoercionTy {})) f m = m { tm_coerce = tm_coerce m |> f } -xtT (D env (ForAllTy (TvBndr tv _) ty)) f m +xtT (D env (ForAllTy (Bndr tv _) ty)) f m = m { tm_forall = tm_forall m |> xtG (D (extendCME env tv) ty) |>> xtBndr env tv f } xtT (D _ ty@(TyConApp _ (_:_))) _ _ = pprPanic "xtT TyConApp" (ppr ty) |