Commit ea5ade34 authored by Ningning Xie's avatar Ningning Xie Committed by Richard Eisenberg

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
parent c23f057f
......@@ -524,7 +524,7 @@ rnIfaceConDecls IfAbstractTyCon = pure IfAbstractTyCon
rnIfaceConDecl :: Rename IfaceConDecl
rnIfaceConDecl d = do
con_name <- rnIfaceGlobal (ifConName d)
con_ex_tvs <- mapM rnIfaceTvBndr (ifConExTvs d)
con_ex_tvs <- mapM rnIfaceBndr (ifConExTCvs d)
con_user_tvbs <- mapM rnIfaceForAllBndr (ifConUserTvBinders d)
let rnIfConEqSpec (n,t) = (,) n <$> rnIfaceType t
con_eq_spec <- mapM rnIfConEqSpec (ifConEqSpec d)
......@@ -535,7 +535,7 @@ rnIfaceConDecl d = do
rnIfaceBang bang = pure bang
con_stricts <- mapM rnIfaceBang (ifConStricts d)
return d { ifConName = con_name
, ifConExTvs = con_ex_tvs
, ifConExTCvs = con_ex_tvs
, ifConUserTvBinders = con_user_tvbs
, ifConEqSpec = con_eq_spec
, ifConCtxt = con_ctxt
......@@ -624,7 +624,7 @@ rnIfaceTvBndr :: Rename IfaceTvBndr
rnIfaceTvBndr (fs, kind) = (,) fs <$> rnIfaceType kind
rnIfaceTyConBinder :: Rename IfaceTyConBinder
rnIfaceTyConBinder (TvBndr tv vis) = TvBndr <$> rnIfaceTvBndr tv <*> pure vis
rnIfaceTyConBinder (Bndr tv vis) = Bndr <$> rnIfaceBndr tv <*> pure vis
rnIfaceAlt :: Rename IfaceAlt
rnIfaceAlt (conalt, names, rhs)
......@@ -656,7 +656,7 @@ rnIfaceCo (IfaceTyConAppCo role tc cos)
rnIfaceCo (IfaceAppCo co1 co2)
= IfaceAppCo <$> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceForAllCo bndr co1 co2)
= IfaceForAllCo <$> rnIfaceTvBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
= IfaceForAllCo <$> rnIfaceBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c)
rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl
rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl
......@@ -711,7 +711,7 @@ rnIfaceType (IfaceCastTy ty co)
= IfaceCastTy <$> rnIfaceType ty <*> rnIfaceCo co
rnIfaceForAllBndr :: Rename IfaceForAllBndr
rnIfaceForAllBndr (TvBndr tv vis) = TvBndr <$> rnIfaceTvBndr tv <*> pure vis
rnIfaceForAllBndr (Bndr tv vis) = Bndr <$> rnIfaceBndr tv <*> pure vis
rnIfaceAppArgs :: Rename IfaceAppArgs
rnIfaceAppArgs (IA_Invis t ts) = IA_Invis <$> rnIfaceType t <*> rnIfaceAppArgs ts
......
......@@ -12,7 +12,7 @@ module ConLike (
, conLikeArity
, conLikeFieldLabels
, conLikeInstOrigArgTys
, conLikeExTyVars
, conLikeExTyCoVars
, conLikeName
, conLikeStupidTheta
, conLikeWrapId_maybe
......@@ -113,10 +113,10 @@ conLikeInstOrigArgTys (RealDataCon data_con) tys =
conLikeInstOrigArgTys (PatSynCon pat_syn) tys =
patSynInstArgTys pat_syn tys
-- | Existentially quantified type variables
conLikeExTyVars :: ConLike -> [TyVar]
conLikeExTyVars (RealDataCon dcon1) = dataConExTyVars dcon1
conLikeExTyVars (PatSynCon psyn1) = patSynExTyVars psyn1
-- | Existentially quantified type/coercion variables
conLikeExTyCoVars :: ConLike -> [TyCoVar]
conLikeExTyCoVars (RealDataCon dcon1) = dataConExTyCoVars dcon1
conLikeExTyCoVars (PatSynCon psyn1) = patSynExTyVars psyn1
conLikeName :: ConLike -> Name
conLikeName (RealDataCon data_con) = dataConName data_con
......@@ -152,7 +152,7 @@ conLikeResTy (PatSynCon ps) tys = patSynInstResTy ps tys
--
-- 1) The universally quantified type variables
--
-- 2) The existentially quantified type variables
-- 2) The existentially quantified type/coercion variables
--
-- 3) The equality specification
--
......@@ -165,7 +165,9 @@ conLikeResTy (PatSynCon ps) tys = patSynInstResTy ps tys
--
-- 7) The original result type
conLikeFullSig :: ConLike
-> ([TyVar], [TyVar], [EqSpec]
-> ([TyVar], [TyCoVar], [EqSpec]
-- Why tyvars for universal but tycovars for existential?
-- See Note [Existential coercion variables] in DataCon
, ThetaType, ThetaType, [Type], Type)
conLikeFullSig (RealDataCon con) =
let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty) = dataConFullSig con
......
This diff is collapsed.
module DataCon where
import GhcPrelude
import Var( TyVar, TyVarBinder )
import Var( TyVar, TyCoVar, TyVarBinder )
import Name( Name, NamedThing )
import {-# SOURCE #-} TyCon( TyCon )
import FieldLabel ( FieldLabel )
......@@ -16,7 +16,7 @@ data EqSpec
dataConName :: DataCon -> Name
dataConTyCon :: DataCon -> TyCon
dataConExTyVars :: DataCon -> [TyVar]
dataConExTyCoVars :: DataCon -> [TyCoVar]
dataConUserTyVars :: DataCon -> [TyVar]
dataConUserTyVarBinders :: DataCon -> [TyVarBinder]
dataConSourceArity :: DataCon -> Arity
......@@ -24,7 +24,7 @@ dataConFieldLabels :: DataCon -> [FieldLabel]
dataConInstOrigArgTys :: DataCon -> [Type] -> [Type]
dataConStupidTheta :: DataCon -> ThetaType
dataConFullSig :: DataCon
-> ([TyVar], [TyVar], [EqSpec], ThetaType, [Type], Type)
-> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Type], Type)
isUnboxedSumCon :: DataCon -> Bool
instance Eq DataCon
......
......@@ -394,7 +394,8 @@ mkDictSelRhs clas val_index
dict_id = mkTemplateLocal 1 pred
arg_ids = mkTemplateLocalsNum 2 arg_tys
rhs_body | new_tycon = unwrapNewTypeBody tycon (mkTyVarTys tyvars) (Var dict_id)
rhs_body | new_tycon = unwrapNewTypeBody tycon (mkTyVarTys tyvars)
(Var dict_id)
| otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
[(DataAlt data_con, arg_ids, varToCoreExpr the_arg_id)]
-- varToCoreExpr needed for equality superclass selectors
......@@ -465,7 +466,7 @@ mkDataConWorkId wkr_name data_con
----------- Workers for newtypes --------------
(nt_tvs, _, nt_arg_tys, _) = dataConSig data_con
res_ty_args = mkTyVarTys nt_tvs
res_ty_args = mkTyCoVarTys nt_tvs
nt_wrap_ty = dataConUserType data_con
nt_work_info = noCafIdInfo -- The NoCaf-ness is set by noCafIdInfo
`setArityInfo` 1 -- Arity 1
......@@ -484,7 +485,7 @@ dataConCPR :: DataCon -> DmdResult
dataConCPR con
| isDataTyCon tycon -- Real data types only; that is,
-- not unboxed tuples or newtypes
, null (dataConExTyVars con) -- No existentials
, null (dataConExTyCoVars con) -- No existentials
, wkr_arity > 0
, wkr_arity <= mAX_CPR_SIZE
= if is_prod then vanillaCprProdRes (dataConRepArity con)
......@@ -631,7 +632,7 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
orig_bangs = dataConSrcBangs data_con
wrap_arg_tys = theta ++ orig_arg_tys
wrap_arity = length wrap_arg_tys
wrap_arity = count isCoVar ex_tvs + length wrap_arg_tys
-- The wrap_args are the arguments *other than* the eq_spec
-- Because we are going to apply the eq_spec args manually in the
-- wrapper
......@@ -672,8 +673,8 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
mk_boxer boxers = DCB (\ ty_args src_vars ->
do { let (ex_vars, term_vars) = splitAtList ex_tvs src_vars
subst1 = zipTvSubst univ_tvs ty_args
subst2 = extendTvSubstList subst1 ex_tvs
(mkTyVarTys ex_vars)
subst2 = extendTCvSubstList subst1 ex_tvs
(mkTyCoVarTys ex_vars)
; (rep_ids, binds) <- go subst2 boxers term_vars
; return (ex_vars ++ rep_ids, binds) } )
......@@ -892,7 +893,8 @@ dataConArgUnpack arg_ty
-- A recursive newtype might mean that
-- 'arg_ty' is a newtype
, let rep_tys = dataConInstArgTys con tc_args
= ASSERT( null (dataConExTyVars con) ) -- Note [Unpacking GADTs and existentials]
= ASSERT( null (dataConExTyCoVars con) )
-- Note [Unpacking GADTs and existentials]
( rep_tys `zip` dataConRepStrictness con
,( \ arg_id ->
do { rep_ids <- mapM newLocal rep_tys
......@@ -959,7 +961,8 @@ isUnpackableType dflags fam_envs ty
unpackable_type ty
| Just (tc, _) <- splitTyConApp_maybe ty
, Just data_con <- tyConSingleAlgDataCon_maybe tc
, null (dataConExTyVars data_con) -- See Note [Unpacking GADTs and existentials]
, null (dataConExTyCoVars data_con)
-- See Note [Unpacking GADTs and existentials]
= Just data_con
| otherwise
= Nothing
......@@ -975,7 +978,7 @@ components, like
And it'd be fine to unpack a product type with existential components
too, but that would require a bit more plumbing, so currently we don't.
So for now we require: null (dataConExTyVars data_con)
So for now we require: null (dataConExTyCoVars data_con)
See Trac #14978
Note [Unpack one-wide fields]
......@@ -1136,7 +1139,7 @@ mkFCallId dflags uniq fcall ty
`setLevityInfoWithType` ty
(bndrs, _) = tcSplitPiTys ty
arity = count isAnonTyBinder bndrs
arity = count isAnonTyCoBinder bndrs
strict_sig = mkClosedStrictSig (replicate arity topDmd) topRes
-- the call does not claim to be strict in its arguments, since they
-- may be lifted (foreign import prim) and the called code doesn't
......
......@@ -79,7 +79,7 @@ data PatSyn
-- Result type
psResultTy :: Type, -- Mentions only psUnivTyVars
-- See Note [Pattern synonym result type]
-- See Note [Pattern synonym result type]
-- See Note [Matchers and builders for pattern synonyms]
psMatcher :: (Id, Bool),
......@@ -339,10 +339,10 @@ instance Data.Data PatSyn where
-- | Build a new pattern synonym
mkPatSyn :: Name
-> Bool -- ^ Is the pattern synonym declared infix?
-> ([TyVarBinder], ThetaType) -- ^ Universially-quantified type variables
-- and required dicts
-> ([TyVarBinder], ThetaType) -- ^ Existentially-quantified type variables
-- and provided dicts
-> ([TyVarBinder], ThetaType) -- ^ Universially-quantified type
-- variables and required dicts
-> ([TyVarBinder], ThetaType) -- ^ Existentially-quantified type
-- variables and provided dicts
-> [Type] -- ^ Original arguments
-> Type -- ^ Original result type
-> (Id, Bool) -- ^ Name of matcher
......
......@@ -61,10 +61,12 @@ module Var (
mustHaveLocalBinding,
-- * TyVar's
TyVarBndr(..), ArgFlag(..), TyVarBinder,
binderVar, binderVars, binderArgFlag, binderKind,
VarBndr(..), ArgFlag(..), TyCoVarBinder, TyVarBinder,
binderVar, binderVars, binderArgFlag, binderType,
isVisibleArgFlag, isInvisibleArgFlag, sameVis,
mkTyCoVarBinder, mkTyCoVarBinders,
mkTyVarBinder, mkTyVarBinders,
isTyVarBinder,
-- ** Constructing TyVar's
mkTyVar, mkTcTyVar,
......@@ -190,7 +192,7 @@ type OutId = Id
Note [Kind and type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before kind polymorphism, TyVar were used to mean type variables. Now
they are use to mean kind *or* type variables. KindVar is used when we
they are used to mean kind *or* type variables. KindVar is used when we
know for sure that it is a kind variable. In future, we might want to
go over the whole compiler code to use:
- TKVar to mean kind or type variables
......@@ -380,7 +382,7 @@ updateVarTypeM f id = do { ty' <- f (varType id)
-- Is something required to appear in source Haskell ('Required'),
-- permitted by request ('Specified') (visible type application), or
-- prohibited entirely from appearing in source Haskell ('Inferred')?
-- See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility] in TyCoRep
-- See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
data ArgFlag = Inferred | Specified | Required
deriving (Eq, Ord, Data)
-- (<) on ArgFlag meant "is less visible than"
......@@ -405,45 +407,68 @@ sameVis _ _ = True
{- *********************************************************************
* *
* TyVarBndr, TyVarBinder
* VarBndr, TyCoVarBinder
* *
********************************************************************* -}
-- Type Variable Binder
-- Variable Binder
--
-- TyVarBndr is polymorphic in both tyvar and visibility fields:
-- * tyvar can be TyVar or IfaceTv
-- * argf can be ArgFlag or TyConBndrVis
data TyVarBndr tyvar argf = TvBndr tyvar argf
-- VarBndr is polymorphic in both var and visibility fields.
-- Currently there are six different uses of 'VarBndr':
-- * Var.TyVarBinder = VarBndr TyVar ArgFlag
-- * Var.TyCoVarBinder = VarBndr TyCoVar ArgFlag
-- * TyCon.TyConBinder = VarBndr TyVar TyConBndrVis
-- * TyCon.TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis
-- * IfaceType.IfaceForAllBndr = VarBndr IfaceBndr ArgFlag
-- * IfaceType.IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
data VarBndr var argf = Bndr var argf
deriving( Data )
-- | Type Variable Binder
-- | Variable Binder
--
-- A 'TyVarBinder' is the binder of a ForAllTy
-- A 'TyCoVarBinder' is the binder of a ForAllTy
-- It's convenient to define this synonym here rather its natural
-- home in TyCoRep, because it's used in DataCon.hs-boot
type TyVarBinder = TyVarBndr TyVar ArgFlag
--
-- A 'TyVarBinder' is a binder with only TyVar
type TyCoVarBinder = VarBndr TyCoVar ArgFlag
type TyVarBinder = VarBndr TyVar ArgFlag
binderVar :: TyVarBndr tv argf -> tv
binderVar (TvBndr v _) = v
binderVar :: VarBndr tv argf -> tv
binderVar (Bndr v _) = v
binderVars :: [TyVarBndr tv argf] -> [tv]
binderVars :: [VarBndr tv argf] -> [tv]
binderVars tvbs = map binderVar tvbs
binderArgFlag :: TyVarBndr tv argf -> argf
binderArgFlag (TvBndr _ argf) = argf
binderArgFlag :: VarBndr tv argf -> argf
binderArgFlag (Bndr _ argf) = argf
binderType :: VarBndr TyCoVar argf -> Type
binderType (Bndr tv _) = varType tv
binderKind :: TyVarBndr TyVar argf -> Kind
binderKind (TvBndr tv _) = tyVarKind tv
-- | Make a named binder
mkTyCoVarBinder :: ArgFlag -> TyCoVar -> TyCoVarBinder
mkTyCoVarBinder vis var = Bndr var vis
-- | Make a named binder
mkTyVarBinder :: ArgFlag -> Var -> TyVarBinder
mkTyVarBinder vis var = TvBndr var vis
-- 'var' should be a type variable
mkTyVarBinder :: ArgFlag -> TyVar -> TyVarBinder
mkTyVarBinder vis var
= ASSERT( isTyVar var )
Bndr var vis
-- | Make many named binders
mkTyCoVarBinders :: ArgFlag -> [TyCoVar] -> [TyCoVarBinder]
mkTyCoVarBinders vis = map (mkTyCoVarBinder vis)
-- | Make many named binders
-- Input vars should be type variables
mkTyVarBinders :: ArgFlag -> [TyVar] -> [TyVarBinder]
mkTyVarBinders vis = map (mkTyVarBinder vis)
isTyVarBinder :: TyCoVarBinder -> Bool
isTyVarBinder (Bndr v _) = isTyVar v
{-
************************************************************************
* *
......@@ -500,20 +525,20 @@ setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar
setTcTyVarDetails tv details = tv { tc_tv_details = details }
-------------------------------------
instance Outputable tv => Outputable (TyVarBndr tv ArgFlag) where
ppr (TvBndr v Required) = ppr v
ppr (TvBndr v Specified) = char '@' <> ppr v
ppr (TvBndr v Inferred) = braces (ppr v)
instance Outputable tv => Outputable (VarBndr tv ArgFlag) where
ppr (Bndr v Required) = ppr v
ppr (Bndr v Specified) = char '@' <> ppr v
ppr (Bndr v Inferred) = braces (ppr v)
instance Outputable ArgFlag where
ppr Required = text "[req]"
ppr Specified = text "[spec]"
ppr Inferred = text "[infrd]"
instance (Binary tv, Binary vis) => Binary (TyVarBndr tv vis) where
put_ bh (TvBndr tv vis) = do { put_ bh tv; put_ bh vis }
instance (Binary tv, Binary vis) => Binary (VarBndr tv vis) where
put_ bh (Bndr tv vis) = do { put_ bh tv; put_ bh vis }
get bh = do { tv <- get bh; vis <- get bh; return (TvBndr tv vis) }
get bh = do { tv <- get bh; vis <- get bh; return (Bndr tv vis) }
instance Binary ArgFlag where
......
......@@ -1037,10 +1037,19 @@ mkEtaWW orig_n orig_expr in_scope orig_ty
| n == 0
= (getTCvInScope subst, reverse eis)
| Just (tv,ty') <- splitForAllTy_maybe ty
, let (subst', tv') = Type.substTyVarBndr subst tv
| Just (tcv,ty') <- splitForAllTy_maybe ty
, let (subst', tcv') = Type.substVarBndr subst tcv
= let ((n_subst, n_tcv), n_n)
-- We want to have at least 'n' lambdas at the top.
-- If tcv is a tyvar, it corresponds to one Lambda (/\).
-- And we won't reduce n.
-- If tcv is a covar, we could eta-expand the expr with one
-- lambda \co:ty. e co. In this case we generate a new variable
-- of the coercion type, update the scope, and reduce n by 1.
| isTyVar tcv = ((subst', tcv'), n)
| otherwise = (freshEtaId n subst' (varType tcv'), n-1)
-- Avoid free vars of the original expression
= go n subst' ty' (EtaVar tv' : eis)
in go n_n n_subst ty' (EtaVar n_tcv : eis)
| Just (arg_ty, res_ty) <- splitFunTy_maybe ty
, not (isTypeLevPoly arg_ty)
......@@ -1123,8 +1132,8 @@ etaBodyForJoinPoint need_args body
= (reverse rev_bs, e)
go n ty subst rev_bs e
| Just (tv, res_ty) <- splitForAllTy_maybe ty
, let (subst', tv') = Type.substTyVarBndr subst tv
= go (n-1) res_ty subst' (tv' : rev_bs) (e `App` Type (mkTyVarTy tv'))
, let (subst', tv') = Type.substVarBndr subst tv
= go (n-1) res_ty subst' (tv' : rev_bs) (e `App` varToCoreExpr tv')
| Just (arg_ty, res_ty) <- splitFunTy_maybe ty
, let (subst', b) = freshEtaId n subst arg_ty
= go (n-1) res_ty subst' (b : rev_bs) (e `App` Var b)
......
......@@ -351,7 +351,7 @@ orphNamesOfType (TyVarTy _) = emptyNameSet
orphNamesOfType (LitTy {}) = emptyNameSet
orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon
`unionNameSet` orphNamesOfTypes tys
orphNamesOfType (ForAllTy bndr res) = orphNamesOfType (binderKind bndr)
orphNamesOfType (ForAllTy bndr res) = orphNamesOfType (binderType bndr)
`unionNameSet` orphNamesOfType res
orphNamesOfType (FunTy arg res) = unitNameSet funTyConName -- NB! See Trac #8535
`unionNameSet` orphNamesOfType arg
......
......@@ -1352,9 +1352,10 @@ lintType ty@(FunTy t1 t2)
; k2 <- lintType t2
; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
lintType t@(ForAllTy (TvBndr tv _vis) ty)
= do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
; lintTyBndr tv $ \tv' ->
lintType t@(ForAllTy (Bndr tv _vis) ty)
-- forall over types
| isTyVar tv
= do { lintTyBndr tv $ \tv' ->
do { k <- lintType ty
; checkValueKind k (text "the body of forall:" <+> ppr t)
; case occCheckExpand [tv'] k of -- See Note [Stupid type synonyms]
......@@ -1364,6 +1365,20 @@ lintType t@(ForAllTy (TvBndr tv _vis) ty)
, text "kind:" <+> ppr k ]))
}}
lintType t@(ForAllTy (Bndr cv _vis) ty)
-- forall over coercions
= do { lintL (isCoVar cv)
(text "Non-Tyvar or Non-Covar bound in type:" <+> ppr t)
; lintL (cv `elemVarSet` tyCoVarsOfType ty)
(text "Covar does not occur in the body:" <+> ppr t)
; lintCoBndr cv $ \_ ->
do { k <- lintType ty
; checkValueKind k (text "the body of forall:" <+> ppr t)
; return liftedTypeKind
-- We don't check variable escape here. Namely, k could refer to cv'
-- See Note [NthCo and newtypes] in TyCoRep
}}
lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
lintType (CastTy ty co)
......@@ -1491,11 +1506,11 @@ lint_app doc kfn kas
addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka)))
; return kfb }
go_app in_scope (ForAllTy (TvBndr kv _vis) kfn) tka@(ta,ka)
= do { let kv_kind = tyVarKind kv
go_app in_scope (ForAllTy (Bndr kv _vis) kfn) tka@(ta,ka)
= do { let kv_kind = varType kv
; unless (ka `eqType` kv_kind) $
addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$ ppr tka)))
; return (substTyWithInScope in_scope [kv] [ta] kfn) }
; return $ substTy (extendTCvSubst (mkEmptyTCvSubst in_scope) kv ta) kfn }
go_app _ kfn ka
= failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ka)))
......@@ -1681,6 +1696,8 @@ lintCoercion co@(AppCo co1 co2)
----------
lintCoercion (ForAllCo tv1 kind_co co)
-- forall over types
| isTyVar tv1
= do { (_, k2) <- lintStarCoercion kind_co
; let tv2 = setTyVarKind tv1 k2
; addInScopeVar tv1 $
......@@ -1700,6 +1717,37 @@ lintCoercion (ForAllCo tv1 kind_co co)
substTy subst t2
; return (k3, k4, tyl, tyr, r) } }
lintCoercion (ForAllCo cv1 kind_co co)
-- forall over coercions
= ASSERT( isCoVar cv1 )
do { (_, k2) <- lintStarCoercion kind_co
; let cv2 = setVarType cv1 k2
; addInScopeVar cv1 $
do {
; (k3, k4, t1, t2, r) <- lintCoercion co
; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co)
; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co)
-- See Note [Weird typing rule for ForAllTy] in Type
; in_scope <- getInScope
; let tyl = mkTyCoInvForAllTy cv1 t1
r2 = coVarRole cv1
kind_co' = downgradeRole r2 Nominal kind_co
eta1 = mkNthCo r2 2 kind_co'
eta2 = mkNthCo r2 3 kind_co'
subst = mkCvSubst in_scope $
-- We need both the free vars of the `t2` and the
-- free vars of the range of the substitution in
-- scope. All the free vars of `t2` and `kind_co` should
-- already be in `in_scope`, because they've been
-- linted and `cv2` has the same unique as `cv1`.
-- See Note [The substitution invariant]
unitVarEnv cv1 (eta1 `mkTransCo` (mkCoVarCo cv2)
`mkTransCo` (mkSymCo eta2))
tyr = mkTyCoInvForAllTy cv2 $
substTy subst t2
; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } }
-- See Note [Weird typing rule for ForAllTy] in Type
lintCoercion co@(FunCo r co1 co2)
= do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
; (k2,k'2,s2,t2,r2) <- lintCoercion co2
......@@ -1804,13 +1852,16 @@ lintCoercion co@(TransCo co1 co2)
lintCoercion the_co@(NthCo r0 n co)
= do { (_, _, s, t, r) <- lintCoercion co
; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
{ (Just (tv_s, _ty_s), Just (tv_t, _ty_t))
| n == 0
{ (Just (tcv_s, _ty_s), Just (tcv_t, _ty_t))
-- works for both tyvar and covar
| n == 0
, (isForAllTy_ty s && isForAllTy_ty t)
|| (isForAllTy_co s && isForAllTy_co t)
-> do { lintRole the_co Nominal r0
; return (ks, kt, ts, tt, r0) }
where
ts = tyVarKind tv_s
tt = tyVarKind tv_t
ts = varType tcv_s
tt = varType tcv_t
ks = typeKind ts
kt = typeKind tt
......@@ -1853,16 +1904,32 @@ lintCoercion (InstCo co arg)
; (k1',k2',s1,s2, r') <- lintCoercion arg
; lintRole arg Nominal r'
; in_scope <- getInScope
; case (splitForAllTy_maybe t1', splitForAllTy_maybe t2') of
(Just (tv1,t1), Just (tv2,t2))
| k1' `eqType` tyVarKind tv1
, k2' `eqType` tyVarKind tv2
-> return (k3, k4,
substTyWithInScope in_scope [tv1] [s1] t1,
substTyWithInScope in_scope [tv2] [s2] t2, r)
| otherwise
-> failWithL (text "Kind mis-match in inst coercion")
_ -> failWithL (text "Bad argument of inst") }
; case (splitForAllTy_ty_maybe t1', splitForAllTy_ty_maybe t2') of
-- forall over tvar
{ (Just (tv1,t1), Just (tv2,t2))
| k1' `eqType` tyVarKind tv1
, k2' `eqType` tyVarKind tv2
-> return (k3, k4,
substTyWithInScope in_scope [tv1] [s1] t1,
substTyWithInScope in_scope [tv2] [s2] t2, r)
| otherwise
-> failWithL (text "Kind mis-match in inst coercion")
; _ -> case (splitForAllTy_co_maybe t1', splitForAllTy_co_maybe t2') of
-- forall over covar
{ (Just (cv1, t1), Just (cv2, t2))
| k1' `eqType` varType cv1
, k2' `eqType` varType cv2
, CoercionTy s1' <- s1
, CoercionTy s2' <- s2
-> do { return $
(liftedTypeKind, liftedTypeKind
-- See Note [Weird typing rule for ForAllTy] in Type
, substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1
, substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2
, r) }
| otherwise
-> failWithL (text "Kind mis-match in inst coercion")
; _ -> failWithL (text "Bad argument of inst") }}}
lintCoercion co@(AxiomInstCo con ind cos)
= do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
......
......@@ -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)
......
......@@ -1010,8 +1010,8 @@ pushCoTyArg co ty
| isReflCo co
= Just (ty, MRefl)
| isForAllTy tyL
= ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
| isForAllTy_ty tyL
= ASSERT2( isForAllTy_ty tyR, ppr co $$ ppr ty )
Just (ty `mkCastTy` co1, MCo co2)
| otherwise
......@@ -1112,11 +1112,11 @@ pushCoDataCon dc dc_args co
= let
tc_arity = tyConArity to_tc
dc_univ_tyvars = dataConUnivTyVars dc
dc_ex_tyvars = dataConExTyVars dc
dc_ex_tcvars = dataConExTyCoVars dc
arg_tys = dataConRepArgTys dc
non_univ_args = dropList dc_univ_tyvars dc_args
(ex_args, val_args) = splitAtList dc_ex_tyvars non_univ_args
(ex_args, val_args) = splitAtList dc_ex_tcvars non_univ_args
-- Make the "Psi" from the paper
omegas = decomposeCo tc_arity co (tyConRolesRepresentational to_tc)
......@@ -1124,7 +1124,7 @@ pushCoDataCon dc dc_args co
= liftCoSubstWithEx Representational
dc_univ_tyvars
omegas
dc_ex_tyvars
dc_ex_tcvars
(map exprToType ex_args)
-- Cast the value arguments (which include dictionaries)
......@@ -1133,7 +1133,7 @@ pushCoDataCon dc dc_args co
to_ex_args = map Type to_ex_arg_tys
dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tyvars,
dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tcvars,
ppr arg_tys, ppr dc_args,
ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc ]
in
......@@ -1179,11 +1179,19 @@ collectBindersPushingCo e
go_lam bs b e co
| isTyVar b
, let Pair tyL tyR = coercionKind co
, ASSERT( isForAllTy tyL )
isForAllTy tyR
, ASSERT( isForAllTy_ty tyL )
isForAllTy_ty tyR
, isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo]
= go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkTyVarTy b)))
| isCoVar b
, let Pair tyL tyR = coercionKind co
, ASSERT( isForAllTy_co tyL )
isForAllTy_co tyR
, isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo]
, let cov = mkCoVarCo b
= go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkCoercionTy cov)))
| isId b
, let Pair tyL tyR = coercionKind co
, ASSERT( isFunTy tyL) isFunTy tyR
......
......@@ -89,7 +89,7 @@ data Subst
TvSubstEnv -- Substitution from TyVars to Types
CvSubstEnv -- Substitution from CoVars to Coercions
-- INVARIANT 1: See TyCORep Note [The substitution invariant]