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/prelude | |
| 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/prelude')
| -rw-r--r-- | compiler/prelude/TysPrim.hs | 8 | ||||
| -rw-r--r-- | compiler/prelude/TysWiredIn.hs | 10 |
2 files changed, 9 insertions, 9 deletions
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs index 30dca25eea..c5af4a5121 100644 --- a/compiler/prelude/TysPrim.hs +++ b/compiler/prelude/TysPrim.hs @@ -96,7 +96,7 @@ import {-# SOURCE #-} TysWiredIn , doubleElemRepDataConTy , mkPromotedListTy ) -import Var ( TyVar, TyVarBndr(TvBndr), mkTyVar ) +import Var ( TyVar, VarBndr(Bndr), mkTyVar ) import Name import TyCon import SrcLoc @@ -351,8 +351,8 @@ funTyConName = mkPrimTyConName (fsLit "->") funTyConKey funTyCon funTyCon :: TyCon funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm where - tc_bndrs = [ TvBndr runtimeRep1TyVar (NamedTCB Inferred) - , TvBndr runtimeRep2TyVar (NamedTCB Inferred) + tc_bndrs = [ Bndr runtimeRep1TyVar (NamedTCB Inferred) + , Bndr runtimeRep2TyVar (NamedTCB Inferred) ] ++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty , tYPE runtimeRep2Ty @@ -598,7 +598,7 @@ GHC sports a veritable menagerie of equality types: class? L/U TyCon ----------------------------------------------------------------------------------------- ~# T U hetero nominal eqPrimTyCon GHC.Prim -~~ C L hetero nominal hEqTyCon GHC.Types +~~ C L hetero nominal heqTyCon GHC.Types ~ C L homo nominal eqTyCon GHC.Types :~: T L homo nominal (not built-in) Data.Type.Equality :~~: T L hetero nominal (not built-in) Data.Type.Equality diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index 740d0d772d..1d47185f02 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -486,8 +486,8 @@ pcDataCon n univs = pcDataConWithFixity False n univs pcDataConWithFixity :: Bool -- ^ declared infix? -> Name -- ^ datacon name -> [TyVar] -- ^ univ tyvars - -> [TyVar] -- ^ ex tyvars - -> [TyVar] -- ^ user-written tyvars + -> [TyCoVar] -- ^ ex tycovars + -> [TyCoVar] -- ^ user-written tycovars -> [Type] -- ^ args -> TyCon -> DataCon @@ -501,7 +501,7 @@ pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (n -- one DataCon unique per pair of Ints. pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo - -> [TyVar] -> [TyVar] -> [TyVar] + -> [TyVar] -> [TyCoVar] -> [TyCoVar] -> [Type] -> TyCon -> DataCon -- The Name should be in the DataName name space; it's the name -- of the DataCon itself. @@ -521,7 +521,7 @@ pcDataConWithFixity' declared_infix dc_name wrk_key rri (map (const no_bang) arg_tys) [] -- No labelled fields tyvars ex_tyvars - (mkTyVarBinders Specified user_tyvars) + (mkTyCoVarBinders Specified user_tyvars) [] -- No equality spec [] -- No theta arg_tys (mkTyConApp tycon (mkTyVarTys tyvars)) @@ -585,7 +585,7 @@ constraintKind = mkTyConApp constraintKindTyCon [] mkFunKind :: Kind -> Kind -> Kind mkFunKind = mkFunTy -mkForAllKind :: TyVar -> ArgFlag -> Kind -> Kind +mkForAllKind :: TyCoVar -> ArgFlag -> Kind -> Kind mkForAllKind = mkForAllTy {- |