Commit e8aa8ccb authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Implement "roles" into GHC.

Roles are a solution to the GeneralizedNewtypeDeriving type-safety
problem.

Roles were first described in the "Generative type abstraction" paper,
by Stephanie Weirich, Dimitrios Vytiniotis, Simon PJ, and Steve Zdancewic.
The implementation is a little different than that paper. For a quick
primer, check out Note [Roles] in Coercion. Also see
http://ghc.haskell.org/trac/ghc/wiki/Roles
and
http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
For a more formal treatment, check out docs/core-spec/core-spec.pdf.

This fixes Trac #1496, #4846, #7148.
parent 303d3de9
......@@ -650,11 +650,12 @@ mkDataCon name declared_infix
| isJust (promotableTyCon_maybe rep_tycon)
-- The TyCon is promotable only if all its datacons
-- are, so the promoteType for prom_kind should succeed
= Just (mkPromotedDataCon con name (getUnique name) prom_kind arity)
= Just (mkPromotedDataCon con name (getUnique name) prom_kind roles)
| otherwise
= Nothing
prom_kind = promoteType (dataConUserType con)
arity = dataConSourceArity con
roles = map (const Nominal) (univ_tvs ++ ex_tvs) ++
map (const Representational) orig_arg_tys
eqSpecPreds :: [(TyVar,Type)] -> ThetaType
eqSpecPreds spec = [ mkEqPred (mkTyVarTy tv) ty | (tv,ty) <- spec ]
......@@ -996,6 +997,7 @@ dataConCannotMatch tys con
\begin{code}
buildAlgTyCon :: Name
-> [TyVar] -- ^ Kind variables and type variables
-> [Role]
-> Maybe CType
-> ThetaType -- ^ Stupid theta
-> AlgTyConRhs
......@@ -1005,14 +1007,14 @@ buildAlgTyCon :: Name
-> TyConParent
-> TyCon
buildAlgTyCon tc_name ktvs cType stupid_theta rhs
buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
is_rec is_promotable gadt_syn parent
= tc
where
kind = mkPiKinds ktvs liftedTypeKind
-- tc and mb_promoted_tc are mutually recursive
tc = mkAlgTyCon tc_name kind ktvs cType stupid_theta
tc = mkAlgTyCon tc_name kind ktvs roles cType stupid_theta
rhs parent is_rec gadt_syn
mb_promoted_tc
......
......@@ -547,7 +547,7 @@ mkDataConRep dflags fam_envs wrap_name data_con
initial_wrap_app = Var (dataConWorkId data_con)
`mkTyApps` res_ty_args
`mkVarApps` ex_tvs
`mkCoApps` map (mkReflCo . snd) eq_spec
`mkCoApps` map (mkReflCo Nominal . snd) eq_spec
-- Dont box the eq_spec coercions since they are
-- marked as HsUnpack by mk_dict_strict_mark
......@@ -823,7 +823,7 @@ wrapNewTypeBody tycon args result_expr
wrapFamInstBody tycon args $
mkCast result_expr (mkSymCo co)
where
co = mkUnbranchedAxInstCo (newTyConCo tycon) args
co = mkUnbranchedAxInstCo Representational (newTyConCo tycon) args
-- When unwrapping, we do *not* apply any family coercion, because this will
-- be done via a CoPat by the type checker. We have to do it this way as
......@@ -833,7 +833,7 @@ wrapNewTypeBody tycon args result_expr
unwrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
unwrapNewTypeBody tycon args result_expr
= ASSERT( isNewTyCon tycon )
mkCast result_expr (mkUnbranchedAxInstCo (newTyConCo tycon) args)
mkCast result_expr (mkUnbranchedAxInstCo Representational (newTyConCo tycon) args)
-- If the type constructor is a representation type of a data instance, wrap
-- the expression into a cast adjusting the expression type, which is an
......@@ -843,7 +843,7 @@ unwrapNewTypeBody tycon args result_expr
wrapFamInstBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
wrapFamInstBody tycon args body
| Just co_con <- tyConFamilyCoercion_maybe tycon
= mkCast body (mkSymCo (mkUnbranchedAxInstCo co_con args))
= mkCast body (mkSymCo (mkUnbranchedAxInstCo Representational co_con args))
| otherwise
= body
......@@ -851,7 +851,7 @@ wrapFamInstBody tycon args body
-- represented by a `CoAxiom`, and not a `TyCon`
wrapTypeFamInstBody :: CoAxiom br -> Int -> [Type] -> CoreExpr -> CoreExpr
wrapTypeFamInstBody axiom ind args body
= mkCast body (mkSymCo (mkAxInstCo axiom ind args))
= mkCast body (mkSymCo (mkAxInstCo Representational axiom ind args))
wrapTypeUnbranchedFamInstBody :: CoAxiom Unbranched -> [Type] -> CoreExpr -> CoreExpr
wrapTypeUnbranchedFamInstBody axiom
......@@ -860,13 +860,13 @@ wrapTypeUnbranchedFamInstBody axiom
unwrapFamInstScrut :: TyCon -> [Type] -> CoreExpr -> CoreExpr
unwrapFamInstScrut tycon args scrut
| Just co_con <- tyConFamilyCoercion_maybe tycon
= mkCast scrut (mkUnbranchedAxInstCo co_con args) -- data instances only
= mkCast scrut (mkUnbranchedAxInstCo Representational co_con args) -- data instances only
| otherwise
= scrut
unwrapTypeFamInstScrut :: CoAxiom br -> Int -> [Type] -> CoreExpr -> CoreExpr
unwrapTypeFamInstScrut axiom ind args scrut
= mkCast scrut (mkAxInstCo axiom ind args)
= mkCast scrut (mkAxInstCo Representational axiom ind args)
unwrapTypeUnbranchedFamInstScrut :: CoAxiom Unbranched -> [Type] -> CoreExpr -> CoreExpr
unwrapTypeUnbranchedFamInstScrut axiom
......
......@@ -16,6 +16,11 @@ module SMRep (
WordOff, ByteOff,
roundUpToWords,
#if __GLASGOW_HASKELL__ > 706
-- ** Immutable arrays of StgWords
UArrayStgWord, listArray, toByteArray,
#endif
-- * Closure repesentation
SMRep(..), -- CmmInfo sees the rep; no one else does
IsStatic,
......@@ -49,8 +54,13 @@ import DynFlags
import Outputable
import Platform
import FastString
import qualified Data.Array.Base as Array
#if __GLASGOW_HASKELL__ > 706
import GHC.Base ( ByteArray# )
import Data.Ix
#endif
import Data.Array.Base
import Data.Char( ord )
import Data.Word
import Data.Bits
......@@ -80,7 +90,11 @@ newtype StgWord = StgWord Word64
#if __GLASGOW_HASKELL__ < 706
Num,
#endif
Bits, IArray UArray)
#if __GLASGOW_HASKELL__ <= 706
Array.IArray Array.UArray,
#endif
Bits)
fromStgWord :: StgWord -> Integer
fromStgWord (StgWord i) = toInteger i
......@@ -125,6 +139,30 @@ hALF_WORD_SIZE_IN_BITS :: DynFlags -> Int
hALF_WORD_SIZE_IN_BITS dflags = platformWordSize (targetPlatform dflags) `shiftL` 2
\end{code}
%************************************************************************
%* *
Immutable arrays of StgWords
%* *
%************************************************************************
\begin{code}
#if __GLASGOW_HASKELL__ > 706
-- TODO: Improve with newtype coercions!
newtype UArrayStgWord i = UArrayStgWord (Array.UArray i Word64)
listArray :: Ix i => (i, i) -> [StgWord] -> UArrayStgWord i
listArray (i,j) words
= UArrayStgWord $ Array.listArray (i,j) (map unStgWord words)
where unStgWord (StgWord w64) = w64
toByteArray :: UArrayStgWord i -> ByteArray#
toByteArray (UArrayStgWord (Array.UArray _ _ _ b)) = b
#endif
\end{code}
%************************************************************************
%* *
......
......@@ -24,7 +24,6 @@ import Demand
import CoreSyn
import CoreFVs
import CoreUtils
import Pair
import Bag
import Literal
import DataCon
......@@ -306,7 +305,8 @@ lintCoreExpr (Lit lit)
lintCoreExpr (Cast expr co)
= do { expr_ty <- lintCoreExpr expr
; co' <- applySubstCo co
; (_, from_ty, to_ty) <- lintCoercion co'
; (_, from_ty, to_ty, r) <- lintCoercion co'
; checkRole co' Representational r
; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
; return to_ty }
......@@ -400,9 +400,9 @@ lintCoreExpr (Type ty)
= pprPanic "lintCoreExpr" (ppr ty)
lintCoreExpr (Coercion co)
= do { co' <- lintInCo co
; let Pair ty1 ty2 = coercionKind co'
; return (mkCoercionType ty1 ty2) }
= do { (_kind, ty1, ty2, role) <- lintInCo co
; checkRole co Nominal role
; return (mkCoercionType role ty1 ty2) }
\end{code}
......@@ -804,49 +804,56 @@ lint_app doc kfn kas
%************************************************************************
\begin{code}
lintInCo :: InCoercion -> LintM OutCoercion
lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
-- Check the coercion, and apply the substitution to it
-- See Note [Linting type lets]
lintInCo co
= addLoc (InCo co) $
do { co' <- applySubstCo co
; _ <- lintCoercion co'
; return co' }
; lintCoercion co' }
lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType)
lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
-- Check the kind of a coercion term, returning the kind
-- Post-condition: the returned OutTypes are lint-free
-- and have the same kind as each other
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoercion (Refl ty)
lintCoercion (Refl r ty)
= do { k <- lintType ty
; return (k, ty, ty) }
; return (k, ty, ty, r) }
lintCoercion co@(TyConAppCo tc cos)
lintCoercion co@(TyConAppCo r tc cos)
| tc `hasKey` funTyConKey
, [co1,co2] <- cos
= do { (k1,s1,t1) <- lintCoercion co1
; (k2,s2,t2) <- lintCoercion co2
= do { (k1,s1,t1,r1) <- lintCoercion co1
; (k2,s2,t2,r2) <- lintCoercion co2
; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
; return (rk, mkFunTy s1 s2, mkFunTy t1 t2) }
; checkRole co1 r r1
; checkRole co2 r r2
; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) }
| otherwise
= do { (ks,ss,ts) <- mapAndUnzip3M lintCoercion cos
= do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos
; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
; return (rk, mkTyConApp tc ss, mkTyConApp tc ts) }
; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs
; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) }
lintCoercion co@(AppCo co1 co2)
= do { (k1,s1,t1) <- lintCoercion co1
; (k2,s2,t2) <- lintCoercion co2
= do { (k1,s1,t1,r1) <- lintCoercion co1
; (k2,s2,t2,r2) <- lintCoercion co2
; rk <- lint_co_app co k1 [(s2,k2)]
; return (rk, mkAppTy s1 s2, mkAppTy t1 t2) }
; if r1 == Phantom
then checkL (r2 == Phantom || r2 == Nominal)
(ptext (sLit "Second argument in AppCo cannot be R:") $$
ppr co)
else checkRole co Nominal r2
; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) }
lintCoercion (ForAllCo tv co)
= do { lintTyBndrKind tv
; (k, s, t) <- addInScopeVar tv (lintCoercion co)
; return (k, mkForAllTy tv s, mkForAllTy tv t) }
; (k, s, t, r) <- addInScopeVar tv (lintCoercion co)
; return (k, mkForAllTy tv s, mkForAllTy tv t, r) }
lintCoercion (CoVarCo cv)
| not (isCoVar cv)
......@@ -857,52 +864,58 @@ lintCoercion (CoVarCo cv)
; cv' <- lookupIdInScope cv
; let (s,t) = coVarKind cv'
k = typeKind s
r = coVarRole cv'
; when (isSuperKind k) $
checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
2 (ppr cv))
; return (k, s, t) }
do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality"))
2 (ppr cv))
; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
2 (ppr cv)) }
; return (k, s, t, r) }
lintCoercion (UnsafeCo ty1 ty2)
lintCoercion (UnivCo r ty1 ty2)
= do { k1 <- lintType ty1
; _k2 <- lintType ty2
-- ; unless (k1 `eqKind` k2) $
-- failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
-- 2 (ppr co))
; return (k1, ty1, ty2) }
; return (k1, ty1, ty2, r) }
lintCoercion (SymCo co)
= do { (k, ty1, ty2) <- lintCoercion co
; return (k, ty2, ty1) }
= do { (k, ty1, ty2, r) <- lintCoercion co
; return (k, ty2, ty1, r) }
lintCoercion co@(TransCo co1 co2)
= do { (k1, ty1a, ty1b) <- lintCoercion co1
; (_, ty2a, ty2b) <- lintCoercion co2
= do { (k1, ty1a, ty1b, r1) <- lintCoercion co1
; (_, ty2a, ty2b, r2) <- lintCoercion co2
; checkL (ty1b `eqType` ty2a)
(hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
; return (k1, ty1a, ty2b) }
; checkRole co r1 r2
; return (k1, ty1a, ty2b, r1) }
lintCoercion the_co@(NthCo n co)
= do { (_,s,t) <- lintCoercion co
= do { (_,s,t,r) <- lintCoercion co
; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
(Just (tc_s, tys_s), Just (tc_t, tys_t))
| tc_s == tc_t
, tys_s `equalLength` tys_t
, n < length tys_s
-> return (ks, ts, tt)
-> return (ks, ts, tt, tr)
where
ts = getNth tys_s n
tt = getNth tys_t n
tr = nthRole r tc_s n
ks = typeKind ts
_ -> failWithL (hang (ptext (sLit "Bad getNth:"))
2 (ppr the_co $$ ppr s $$ ppr t)) }
lintCoercion the_co@(LRCo lr co)
= do { (_,s,t) <- lintCoercion co
= do { (_,s,t,r) <- lintCoercion co
; checkRole co Nominal r
; case (splitAppTy_maybe s, splitAppTy_maybe t) of
(Just s_pr, Just t_pr)
-> return (k, s_pick, t_pick)
-> return (k, s_pick, t_pick, Nominal)
where
s_pick = pickLR lr s_pr
t_pick = pickLR lr t_pr
......@@ -912,13 +925,13 @@ lintCoercion the_co@(LRCo lr co)
2 (ppr the_co $$ ppr s $$ ppr t)) }
lintCoercion (InstCo co arg_ty)
= do { (k,s,t) <- lintCoercion co
; arg_kind <- lintType arg_ty
= do { (k,s,t,r) <- lintCoercion co
; arg_kind <- lintType arg_ty
; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
(Just (tv1,ty1), Just (tv2,ty2))
| arg_kind `isSubKind` tyVarKind tv1
-> return (k, substTyWith [tv1] [arg_ty] ty1,
substTyWith [tv2] [arg_ty] ty2)
substTyWith [tv2] [arg_ty] ty2, r)
| otherwise
-> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
_ -> failWithL (ptext (sLit "Bad argument of inst")) }
......@@ -927,27 +940,29 @@ lintCoercion co@(AxiomInstCo con ind cos)
= do { unless (0 <= ind && ind < brListLength (coAxiomBranches con))
(bad_ax (ptext (sLit "index out of range")))
-- See Note [Kind instantiation in coercions]
; let CoAxBranch { cab_tvs = ktvs
, cab_lhs = lhs
, cab_rhs = rhs } = coAxiomNthBranch con ind
; let CoAxBranch { cab_tvs = ktvs
, cab_roles = roles
, cab_lhs = lhs
, cab_rhs = rhs } = coAxiomNthBranch con ind
; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
; in_scope <- getInScope
; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
; (subst_l, subst_r) <- foldlM check_ki
(empty_subst, empty_subst)
(ktvs `zip` cos)
(zip3 ktvs roles cos)
; let lhs' = Type.substTys subst_l lhs
rhs' = Type.substTy subst_r rhs
; case checkAxInstCo co of
Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch)
Nothing -> return ()
; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs') }
; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) }
where
bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
2 (ppr co))
check_ki (subst_l, subst_r) (ktv, co)
= do { (k, t1, t2) <- lintCoercion co
check_ki (subst_l, subst_r) (ktv, role, co)
= do { (k, t1, t2, r) <- lintCoercion co
; checkRole co role r
; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
-- Using subst_l is ok, because subst_l and subst_r
-- must agree on kind equalities
......@@ -955,6 +970,11 @@ lintCoercion co@(AxiomInstCo con ind cos)
(bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
; return (Type.extendTvSubst subst_l ktv t1,
Type.extendTvSubst subst_r ktv t2) }
lintCoercion co@(SubCo co')
= do { (k,s,t,r) <- lintCoercion co'
; checkRole co Nominal r
; return (k,s,t,Representational) }
\end{code}
%************************************************************************
......@@ -1131,6 +1151,17 @@ checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
-- annotations need only be consistent, not equal)
-- Assumes ty1,ty2 are have alrady had the substitution applied
checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
checkRole :: Coercion
-> Role -- expected
-> Role -- actual
-> LintM ()
checkRole co r1 r2
= checkL (r1 == r2)
(ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
ptext (sLit "got") <+> ppr r2 $$
ptext (sLit "in") <+> ppr co)
\end{code}
%************************************************************************
......
......@@ -1163,7 +1163,7 @@ data ConCont = CC [CoreExpr] Coercion
-- where t1..tk are the *universally-qantified* type args of 'dc'
exprIsConApp_maybe :: InScopeEnv -> CoreExpr -> Maybe (DataCon, [Type], [CoreExpr])
exprIsConApp_maybe (in_scope, id_unf) expr
= go (Left in_scope) expr (CC [] (mkReflCo (exprType expr)))
= go (Left in_scope) expr (CC [] (mkReflCo Representational (exprType expr)))
where
go :: Either InScopeSet Subst
-> CoreExpr -> ConCont
......@@ -1252,9 +1252,11 @@ dealWithCoercion co dc dc_args
-- Make the "theta" from Fig 3 of the paper
gammas = decomposeCo tc_arity co
theta_subst = liftCoSubstWith
theta_subst = liftCoSubstWith Representational
(dc_univ_tyvars ++ dc_ex_tyvars)
(gammas ++ map mkReflCo (stripTypeArgs ex_args))
-- existentials are at role N
(gammas ++ map (mkReflCo Nominal)
(stripTypeArgs ex_args))
-- Cast the value arguments (which include dictionaries)
new_val_args = zipWith cast_arg arg_tys val_args
......
......@@ -187,9 +187,12 @@ mkCast (Coercion e_co) co
= Coercion (mkCoCast e_co co)
mkCast (Cast expr co2) co
= ASSERT(let { Pair from_ty _to_ty = coercionKind co;
Pair _from_ty2 to_ty2 = coercionKind co2} in
from_ty `eqType` to_ty2 )
= WARN(let { Pair from_ty _to_ty = coercionKind co;
Pair _from_ty2 to_ty2 = coercionKind co2} in
not (from_ty `eqType` to_ty2),
vcat ([ ptext (sLit "expr:") <+> ppr expr
, ptext (sLit "co2:") <+> ppr co2
, ptext (sLit "co:") <+> ppr co ]) )
mkCast expr (mkTransCo co2 co)
mkCast expr co
......@@ -1602,7 +1605,7 @@ need to address that here.
\begin{code}
tryEtaReduce :: [Var] -> CoreExpr -> Maybe CoreExpr
tryEtaReduce bndrs body
= go (reverse bndrs) body (mkReflCo (exprType body))
= go (reverse bndrs) body (mkReflCo Representational (exprType body))
where
incoming_arity = count isId bndrs
......@@ -1659,9 +1662,10 @@ tryEtaReduce bndrs body
| Just tv <- getTyVar_maybe ty
, bndr == tv = Just (mkForAllCo tv co)
ok_arg bndr (Var v) co
| bndr == v = Just (mkFunCo (mkReflCo (idType bndr)) co)
| bndr == v = Just (mkFunCo Representational
(mkReflCo Representational (idType bndr)) co)
ok_arg bndr (Cast (Var v) co_arg) co
| bndr == v = Just (mkFunCo (mkSymCo co_arg) co)
| bndr == v = Just (mkFunCo Representational (mkSymCo co_arg) co)
-- The simplifier combines multiple casts into one,
-- so we can have a simple-minded pattern match here
ok_arg _ _ _ = Nothing
......
......@@ -34,7 +34,7 @@ data Exp
| Lam Bind Exp
| Let Vdefg Exp
| Case Exp Vbind Ty [Alt] {- non-empty list -}
| Cast Exp Ty
| Cast Exp Coercion
| Tick String Exp {- XXX probably wrong -}
| External String String Ty {- target name, convention, and type -}
| DynExternal String Ty {- convention and type (incl. Addr# of target as first arg) -}
......@@ -52,23 +52,30 @@ data Alt
type Vbind = (Var,Ty)
type Tbind = (Tvar,Kind)
-- Internally, we represent types and coercions separately; but for
-- the purposes of external core (at least for now) it's still
-- convenient to collapse them into a single type.
data Ty
= Tvar Tvar
| Tcon (Qual Tcon)
| Tapp Ty Ty
| Tforall Tbind Ty
data Coercion
-- We distinguish primitive coercions because External Core treats
-- them specially, so we have to print them out with special syntax.
| TransCoercion Ty Ty
| SymCoercion Ty
| UnsafeCoercion Ty Ty
| InstCoercion Ty Ty
| NthCoercion Int Ty
| AxiomCoercion (Qual Tcon) Int [Ty]
| LRCoercion LeftOrRight Ty
= ReflCoercion Role Ty
| SymCoercion Coercion
| TransCoercion Coercion Coercion
| TyConAppCoercion Role (Qual Tcon) [Coercion]
| AppCoercion Coercion Coercion
| ForAllCoercion Tbind Coercion
| CoVarCoercion Var
| UnivCoercion Role Ty Ty
| InstCoercion Coercion Ty
| NthCoercion Int Coercion
| AxiomCoercion (Qual Tcon) Int [Coercion]
| LRCoercion LeftOrRight Coercion
| SubCoercion Coercion
data Role = Nominal | Representational | Phantom
data LeftOrRight = CLeft | CRight
......
......@@ -309,29 +309,29 @@ make_var_qid dflags force_unqual = make_qid dflags force_unqual True
make_con_qid :: DynFlags -> Name -> C.Qual C.Id
make_con_qid dflags = make_qid dflags False False
make_co :: DynFlags -> Coercion -> C.Ty
make_co dflags (Refl ty) = make_ty dflags ty
make_co dflags (TyConAppCo tc cos) = make_conAppCo dflags (qtc dflags tc) cos
make_co dflags (AppCo c1 c2) = C.Tapp (make_co dflags c1) (make_co dflags c2)
make_co dflags (ForAllCo tv co) = C.Tforall (make_tbind tv) (make_co dflags co)
make_co _ (CoVarCo cv) = C.Tvar (make_var_id (coVarName cv))
make_co :: DynFlags -> Coercion -> C.Coercion
make_co dflags (Refl r ty) = C.ReflCoercion (make_role r) $ make_ty dflags ty
make_co dflags (TyConAppCo r tc cos) = C.TyConAppCoercion (make_role r) (qtc dflags tc) (map (make_co dflags) cos)
make_co dflags (AppCo c1 c2) = C.AppCoercion (make_co dflags c1) (make_co dflags c2)
make_co dflags (ForAllCo tv co) = C.ForAllCoercion (make_tbind tv) (make_co dflags co)
make_co _ (CoVarCo cv) = C.CoVarCoercion (make_var_id (coVarName cv))
make_co dflags (AxiomInstCo cc ind cos) = C.AxiomCoercion (qcc dflags cc) ind (map (make_co dflags) cos)
make_co dflags (UnsafeCo t1 t2) = C.UnsafeCoercion (make_ty dflags t1) (make_ty dflags t2)
make_co dflags (UnivCo r t1 t2) = C.UnivCoercion (make_role r) (make_ty dflags t1) (make_ty dflags t2)
make_co dflags (SymCo co) = C.SymCoercion (make_co dflags co)
make_co dflags (TransCo c1 c2) = C.TransCoercion (make_co dflags c1) (make_co dflags c2)
make_co dflags (NthCo d co) = C.NthCoercion d (make_co dflags co)
make_co dflags (LRCo lr co) = C.LRCoercion (make_lr lr) (make_co dflags co)
make_co dflags (InstCo co ty) = C.InstCoercion (make_co dflags co) (make_ty dflags ty)
make_co dflags (SubCo co) = C.SubCoercion (make_co dflags co)
make_lr :: LeftOrRight -> C.LeftOrRight
make_lr CLeft = C.CLeft
make_lr CRight = C.CRight
-- Used for both tycon app coercions and axiom instantiations.
make_conAppCo :: DynFlags -> C.Qual C.Tcon -> [Coercion] -> C.Ty
make_conAppCo dflags con cos =
foldl C.Tapp (C.Tcon con)
(map (make_co dflags) cos)
make_role :: Role -> C.Role
make_role Nominal = C.Nominal
make_role Representational = C.Representational
make_role Phantom = C.Phantom
-------
isALocal :: Name -> CoreM Bool
......
......@@ -102,22 +102,6 @@ pbty t = paty t
pty (Tapp(Tapp(Tcon tc) t1) t2) | tc == tcArrow = fsep [pbty t1, text "->",pty t2]
pty (Tforall tb t) = text "%forall" <+> pforall [tb] t
pty (TransCoercion t1 t2) =
sep [text "%trans", paty t1, paty t2]
pty (SymCoercion t) =
sep [text "%sym", paty t]
pty (UnsafeCoercion t1 t2) =
sep [text "%unsafe", paty t1, paty t2]
pty (NthCoercion n t) =
sep [text "%nth", int n, paty t]
pty (LRCoercion CLeft t) =
sep [text "%left", paty t]
pty (LRCoercion CRight t) =
sep [text "%right", paty t]
pty (InstCoercion t1 t2) =
sep [text "%inst", paty t1, paty t2]
pty (AxiomCoercion tc i cos) =
pqname tc <+> int i <+> sep (map paty cos)
pty ty@(Tapp {}) = pappty ty []
pty ty@(Tvar {}) = paty ty
pty ty@(Tcon {}) = paty ty
......@@ -130,6 +114,48 @@ pforall :: [Tbind] -> Ty -> Doc
pforall tbs (Tforall tb t) = pforall (tbs ++ [tb]) t
pforall tbs t = hsep (map ptbind tbs) <+> char '.' <+> pty t
paco, pbco, pco :: Coercion -> Doc
paco (ReflCoercion r ty) = char '<' <> pty ty <> text ">_" <> prole r
paco (TyConAppCoercion r qtc []) = pqname qtc <> char '_' <> prole r
paco (AxiomCoercion qtc i []) = pqname qtc <> char '[' <> int i <> char ']'
paco (CoVarCoercion cv) = pname cv
paco c = parens (pco c)
pbco (TyConAppCoercion _ arr [co1, co2])
| arr == tcArrow
= parens (fsep [pbco co1, text "->", pco co2])
pbco co = paco co
pco c@(ReflCoercion {}) = paco c
pco (SymCoercion co) = sep [text "%sub", paco co]
pco (TransCoercion co1 co2) = sep [text "%trans", paco co1, paco co2]
pco (TyConAppCoercion _ arr [co1, co2])
| arr == tcArrow = fsep [pbco co1, text "->", pco co2]
pco (TyConAppCoercion r qtc cos) = parens (pqname qtc <+> sep (map paco cos)) <> char '_' <> prole r
pco co@(AppCoercion {}) = pappco co []
pco (ForAllCoercion tb co) = text "%forall" <+> pforallco [tb] co
pco co@(CoVarCoercion {}) = paco co
pco (UnivCoercion r ty1 ty2) = sep [text "%univ", prole r, paty ty1, paty ty2]
pco (InstCoercion co ty) = sep [text "%inst", paco co, paty ty]
pco (NthCoercion i co) = sep [text "%nth", int i, paco co]
pco (AxiomCoercion qtc i cos) = pqname qtc <> char '[' <> int i <> char ']' <+> sep (map paco cos)
pco (LRCoercion CLeft co) = sep [text "%left", paco co]
pco (LRCoercion CRight co) = sep [text "%right", paco co]
pco (SubCoercion co) = sep [text "%sub", paco co]
pappco :: Coercion -> [Coercion ] -> Doc
pappco (AppCoercion co1 co2) cos = pappco co1 (co2:cos)
pappco co cos = sep (map paco (co:cos))
pforallco :: [Tbind] -> Coercion -> Doc
pforallco tbs (ForAllCoercion tb co) = pforallco (tbs ++ [tb]) co
pforallco tbs co = hsep (map ptbind tbs) <+> char '.' <+> pco co