module TcEvidence (
HsWrapper(..),
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,
TcEvBinds(..), EvBindsVar(..),
EvBindMap(..), emptyEvBindMap, extendEvBinds,
lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
isEmptyEvBindMap,
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
evBindVar, isCoEvBindsVar,
EvTerm(..), EvExpr,
evId, evCoercion, evCast, evDFunApp, evDataConApp, evSelector,
mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
evTermCoercion, evTermCoercion_maybe,
EvCallStack(..),
EvTypeable(..),
TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
Role(..), LeftOrRight(..), pickLR,
mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
tcDowngradeRole,
mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflLeftCo, mkTcPhantomCo,
mkTcCoherenceLeftCo,
mkTcCoherenceRightCo,
mkTcKindCo,
tcCoercionKind, coVarsOfTcCo,
mkTcCoVarCo,
isTcReflCo, isTcReflexiveCo,
tcCoercionRole,
unwrapIP, wrapIP
) where
#include "HsVersions.h"
import GhcPrelude
import Var
import CoAxiom
import Coercion
import PprCore ()
import TcType
import Type
import TyCon
import DataCon( DataCon, dataConWrapId )
import Class( Class )
import PrelNames
import DynFlags ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
import VarEnv
import VarSet
import Name
import Pair
import CoreSyn
import Class ( classSCSelId )
import Id ( isEvVar )
import CoreFVs ( exprSomeFreeVars )
import Util
import Bag
import qualified Data.Data as Data
import Outputable
import SrcLoc
import Data.IORef( IORef )
import UniqSet
type TcCoercion = Coercion
type TcCoercionN = CoercionN
type TcCoercionR = CoercionR
type TcCoercionP = CoercionP
mkTcReflCo :: Role -> TcType -> TcCoercion
mkTcSymCo :: TcCoercion -> TcCoercion
mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
mkTcNomReflCo :: TcType -> TcCoercionN
mkTcRepReflCo :: TcType -> TcCoercionR
mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion
mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex
-> [TcType] -> [TcCoercion] -> TcCoercion
mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
-> [TcCoercion] -> TcCoercionR
mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcSubCo :: TcCoercionN -> TcCoercionR
maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcGReflLeftCo :: Role -> TcType -> TcCoercionN -> TcCoercion
mkTcCoherenceLeftCo :: Role -> TcType -> TcCoercionN
-> TcCoercion -> TcCoercion
mkTcCoherenceRightCo :: Role -> TcType -> TcCoercionN
-> TcCoercion -> TcCoercion
mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP
mkTcKindCo :: TcCoercion -> TcCoercionN
mkTcCoVarCo :: CoVar -> TcCoercion
tcCoercionKind :: TcCoercion -> Pair TcType
tcCoercionRole :: TcCoercion -> Role
coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet
isTcReflCo :: TcCoercion -> Bool
isTcReflexiveCo :: TcCoercion -> Bool
mkTcReflCo = mkReflCo
mkTcSymCo = mkSymCo
mkTcTransCo = mkTransCo
mkTcNomReflCo = mkNomReflCo
mkTcRepReflCo = mkRepReflCo
mkTcTyConAppCo = mkTyConAppCo
mkTcAppCo = mkAppCo
mkTcFunCo = mkFunCo
mkTcAxInstCo = mkAxInstCo
mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational
mkTcForAllCo = mkForAllCo
mkTcForAllCos = mkForAllCos
mkTcNthCo = mkNthCo
mkTcLRCo = mkLRCo
mkTcSubCo = mkSubCo
maybeTcSubCo = maybeSubCo
tcDowngradeRole = downgradeRole
mkTcAxiomRuleCo = mkAxiomRuleCo
mkTcGReflRightCo = mkGReflRightCo
mkTcGReflLeftCo = mkGReflLeftCo
mkTcCoherenceLeftCo = mkCoherenceLeftCo
mkTcCoherenceRightCo = mkCoherenceRightCo
mkTcPhantomCo = mkPhantomCo
mkTcKindCo = mkKindCo
mkTcCoVarCo = mkCoVarCo
tcCoercionKind = coercionKind
tcCoercionRole = coercionRole
coVarsOfTcCo = coVarsOfCo
isTcReflCo = isReflCo
isTcReflexiveCo = isReflexiveCo
data HsWrapper
= WpHole
| WpCompose HsWrapper HsWrapper
| WpFun HsWrapper HsWrapper TcType SDoc
| WpCast TcCoercionR
| WpEvLam EvVar
| WpEvApp EvTerm
| WpTyLam TyVar
| WpTyApp KindOrType
| WpLet TcEvBinds
instance Data.Data HsWrapper where
gfoldl _ z WpHole = z WpHole
gfoldl k z (WpCompose a1 a2) = z WpCompose `k` a1 `k` a2
gfoldl k z (WpFun a1 a2 a3 _) = z wpFunEmpty `k` a1 `k` a2 `k` a3
gfoldl k z (WpCast a1) = z WpCast `k` a1
gfoldl k z (WpEvLam a1) = z WpEvLam `k` a1
gfoldl k z (WpEvApp a1) = z WpEvApp `k` a1
gfoldl k z (WpTyLam a1) = z WpTyLam `k` a1
gfoldl k z (WpTyApp a1) = z WpTyApp `k` a1
gfoldl k z (WpLet a1) = z WpLet `k` a1
gunfold k z c = case Data.constrIndex c of
1 -> z WpHole
2 -> k (k (z WpCompose))
3 -> k (k (k (z wpFunEmpty)))
4 -> k (z WpCast)
5 -> k (z WpEvLam)
6 -> k (z WpEvApp)
7 -> k (z WpTyLam)
8 -> k (z WpTyApp)
_ -> k (z WpLet)
toConstr WpHole = wpHole_constr
toConstr (WpCompose _ _) = wpCompose_constr
toConstr (WpFun _ _ _ _) = wpFun_constr
toConstr (WpCast _) = wpCast_constr
toConstr (WpEvLam _) = wpEvLam_constr
toConstr (WpEvApp _) = wpEvApp_constr
toConstr (WpTyLam _) = wpTyLam_constr
toConstr (WpTyApp _) = wpTyApp_constr
toConstr (WpLet _) = wpLet_constr
dataTypeOf _ = hsWrapper_dataType
hsWrapper_dataType :: Data.DataType
hsWrapper_dataType
= Data.mkDataType "HsWrapper"
[ wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr
, wpEvLam_constr, wpEvApp_constr, wpTyLam_constr, wpTyApp_constr
, wpLet_constr]
wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr,
wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr :: Data.Constr
wpHole_constr = mkHsWrapperConstr "WpHole"
wpCompose_constr = mkHsWrapperConstr "WpCompose"
wpFun_constr = mkHsWrapperConstr "WpFun"
wpCast_constr = mkHsWrapperConstr "WpCast"
wpEvLam_constr = mkHsWrapperConstr "WpEvLam"
wpEvApp_constr = mkHsWrapperConstr "WpEvApp"
wpTyLam_constr = mkHsWrapperConstr "WpTyLam"
wpTyApp_constr = mkHsWrapperConstr "WpTyApp"
wpLet_constr = mkHsWrapperConstr "WpLet"
mkHsWrapperConstr :: String -> Data.Constr
mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix
wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper
wpFunEmpty c1 c2 t1 = WpFun c1 c2 t1 empty
(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
WpHole <.> c = c
c <.> WpHole = c
c1 <.> c2 = c1 `WpCompose` c2
mkWpFun :: HsWrapper -> HsWrapper
-> TcType
-> TcType
-> SDoc
-> HsWrapper
mkWpFun WpHole WpHole _ _ _ = WpHole
mkWpFun WpHole (WpCast co2) t1 _ _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
mkWpFun (WpCast co1) WpHole _ t2 _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
mkWpFun (WpCast co1) (WpCast co2) _ _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
mkWpFun co1 co2 t1 _ d = WpFun co1 co2 t1 d
mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper
mkWpFuns args res_ty res_wrap doc = snd $ go args res_ty res_wrap
where
go [] res_ty res_wrap = (res_ty, res_wrap)
go ((arg_ty, arg_wrap) : args) res_ty res_wrap
= let (tail_ty, tail_wrap) = go args res_ty res_wrap in
(arg_ty `mkFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty doc)
mkWpCastR :: TcCoercionR -> HsWrapper
mkWpCastR co
| isTcReflCo co = WpHole
| otherwise = ASSERT2(tcCoercionRole co == Representational, ppr co)
WpCast co
mkWpCastN :: TcCoercionN -> HsWrapper
mkWpCastN co
| isTcReflCo co = WpHole
| otherwise = ASSERT2(tcCoercionRole co == Nominal, ppr co)
WpCast (mkTcSubCo co)
mkWpTyApps :: [Type] -> HsWrapper
mkWpTyApps tys = mk_co_app_fn WpTyApp tys
mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvApps args = mk_co_app_fn WpEvApp args
mkWpEvVarApps :: [EvVar] -> HsWrapper
mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
mkWpTyLams :: [TyVar] -> HsWrapper
mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
mkWpLams :: [Var] -> HsWrapper
mkWpLams ids = mk_co_lam_fn WpEvLam ids
mkWpLet :: TcEvBinds -> HsWrapper
mkWpLet (EvBinds b) | isEmptyBag b = WpHole
mkWpLet ev_binds = WpLet ev_binds
mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
idHsWrapper :: HsWrapper
idHsWrapper = WpHole
isIdHsWrapper :: HsWrapper -> Bool
isIdHsWrapper WpHole = True
isIdHsWrapper _ = False
collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
collectHsWrapBinders wrap = go wrap []
where
go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
go (WpEvLam v) wraps = add_lam v (gos wraps)
go (WpTyLam v) wraps = add_lam v (gos wraps)
go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
go wrap wraps = ([], foldl' (<.>) wrap wraps)
gos [] = ([], WpHole)
gos (w:ws) = go w ws
add_lam v (vs,w) = (v:vs, w)
data TcEvBinds
= TcEvBinds
EvBindsVar
| EvBinds
(Bag EvBind)
data EvBindsVar
= EvBindsVar {
ebv_uniq :: Unique,
ebv_binds :: IORef EvBindMap,
ebv_tcvs :: IORef CoVarSet
}
| CoEvBindsVar {
ebv_uniq :: Unique,
ebv_tcvs :: IORef CoVarSet
}
instance Data.Data TcEvBinds where
toConstr _ = abstractConstr "TcEvBinds"
gunfold _ _ = error "gunfold"
dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
isCoEvBindsVar :: EvBindsVar -> Bool
isCoEvBindsVar (CoEvBindsVar {}) = True
isCoEvBindsVar (EvBindsVar {}) = False
newtype EvBindMap
= EvBindMap {
ev_bind_varenv :: DVarEnv EvBind
}
emptyEvBindMap :: EvBindMap
emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
extendEvBinds bs ev_bind
= EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
(eb_lhs ev_bind)
ev_bind }
isEmptyEvBindMap :: EvBindMap -> Bool
isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
evBindMapBinds :: EvBindMap -> Bag EvBind
evBindMapBinds = foldEvBindMap consBag emptyBag
foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
filterEvBindMap k (EvBindMap { ev_bind_varenv = env })
= EvBindMap { ev_bind_varenv = filterDVarEnv k env }
instance Outputable EvBindMap where
ppr (EvBindMap m) = ppr m
data EvBind
= EvBind { eb_lhs :: EvVar
, eb_rhs :: EvTerm
, eb_is_given :: Bool
}
evBindVar :: EvBind -> EvVar
evBindVar = eb_lhs
mkWantedEvBind :: EvVar -> EvTerm -> EvBind
mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
mkGivenEvBind :: EvVar -> EvTerm -> EvBind
mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
data EvTerm
= EvExpr EvExpr
| EvTypeable Type EvTypeable
| EvFun
{ et_tvs :: [TyVar]
, et_given :: [EvVar]
, et_binds :: TcEvBinds
, et_body :: EvVar }
deriving Data.Data
type EvExpr = CoreExpr
evId :: EvId -> EvExpr
evId = Var
evCoercion :: TcCoercion -> EvTerm
evCoercion co = EvExpr (Coercion co)
evCast :: EvExpr -> TcCoercion -> EvTerm
evCast et tc | isReflCo tc = EvExpr et
| otherwise = EvExpr (Cast et tc)
evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets
evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp dc tys ets = evDFunApp (dataConWrapId dc) tys ets
evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
evTypeable :: Type -> EvTypeable -> EvTerm
evTypeable = EvTypeable
data EvTypeable
= EvTypeableTyCon TyCon [EvTerm]
| EvTypeableTyApp EvTerm EvTerm
| EvTypeableTrFun EvTerm EvTerm
| EvTypeableTyLit EvTerm
deriving Data.Data
data EvCallStack
= EvCsEmpty
| EvCsPushCall Name RealSrcSpan EvExpr
deriving Data.Data
mkEvCast :: EvExpr -> TcCoercion -> EvTerm
mkEvCast ev lco
| ASSERT2( tcCoercionRole lco == Representational
, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
isTcReflCo lco = EvExpr ev
| otherwise = evCast ev lco
mkEvScSelectors
:: Class -> [TcType]
-> [(TcPredType,
EvExpr)
]
mkEvScSelectors cls tys
= zipWith mk_pr (immSuperClasses cls tys) [0..]
where
mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys)
where
sc_sel_id = classSCSelId cls i
emptyTcEvBinds :: TcEvBinds
emptyTcEvBinds = EvBinds emptyBag
isEmptyTcEvBinds :: TcEvBinds -> Bool
isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
evTermCoercion_maybe ev_term
| EvExpr e <- ev_term = go e
| otherwise = Nothing
where
go :: EvExpr -> Maybe TcCoercion
go (Var v) = return (mkCoVarCo v)
go (Coercion co) = return co
go (Cast tm co) = do { co' <- go tm
; return (mkCoCast co' co) }
go _ = Nothing
evTermCoercion :: EvTerm -> TcCoercion
evTermCoercion tm = case evTermCoercion_maybe tm of
Just co -> co
Nothing -> pprPanic "evTermCoercion" (ppr tm)
findNeededEvVars :: EvBindMap -> VarSet -> VarSet
findNeededEvVars ev_binds seeds
= transCloVarSet also_needs seeds
where
also_needs :: VarSet -> VarSet
also_needs needs = nonDetFoldUniqSet add emptyVarSet needs
add :: Var -> VarSet -> VarSet
add v needs
| Just ev_bind <- lookupEvBind ev_binds v
, EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
, is_given
= evVarsOfTerm rhs `unionVarSet` needs
| otherwise
= needs
evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
evVarsOfTerm (EvFun {}) = emptyVarSet
evVarsOfTerms :: [EvTerm] -> VarSet
evVarsOfTerms = mapUnionVarSet evVarsOfTerm
evVarsOfTypeable :: EvTypeable -> VarSet
evVarsOfTypeable ev =
case ev of
EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e
EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
EvTypeableTyLit e -> evVarsOfTerm e
instance Outputable HsWrapper where
ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
pprHsWrapper wrap pp_thing_inside
= sdocWithDynFlags $ \ dflags ->
if gopt Opt_PrintTypecheckerElaboration dflags
then help pp_thing_inside wrap False
else pp_thing_inside False
where
help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
help it WpHole = it
help it (WpCompose f1 f2) = help (help it f2) f1
help it (WpFun f1 f2 t1 _) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
<+> pprParendCo co)]
help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <+> pprParendType ty]
help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pprLamBndr id <> dot, it False]
help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pprLamBndr tv <> dot, it False]
help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
pprLamBndr :: Id -> SDoc
pprLamBndr v = pprBndr LambdaBind v
add_parens, no_parens :: SDoc -> Bool -> SDoc
add_parens d True = parens d
add_parens d False = d
no_parens d _ = d
instance Outputable TcEvBinds where
ppr (TcEvBinds v) = ppr v
ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
instance Outputable EvBindsVar where
ppr (EvBindsVar { ebv_uniq = u })
= text "EvBindsVar" <> angleBrackets (ppr u)
ppr (CoEvBindsVar { ebv_uniq = u })
= text "CoEvBindsVar" <> angleBrackets (ppr u)
instance Uniquable EvBindsVar where
getUnique = ebv_uniq
instance Outputable EvBind where
ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
= sep [ pp_gw <+> ppr v
, nest 2 $ equals <+> ppr e ]
where
pp_gw = brackets (if is_given then char 'G' else char 'W')
instance Outputable EvTerm where
ppr (EvExpr e) = ppr e
ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
ppr (EvFun { et_tvs = tvs, et_given = gs, et_binds = bs, et_body = w })
= hang (text "\\" <+> sep (map pprLamBndr (tvs ++ gs)) <+> arrow)
2 (ppr bs $$ ppr w)
instance Outputable EvCallStack where
ppr EvCsEmpty
= text "[]"
ppr (EvCsPushCall name loc tm)
= ppr (name,loc) <+> text ":" <+> ppr tm
instance Outputable EvTypeable where
ppr (EvTypeableTyCon ts _) = text "TyCon" <+> ppr ts
ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2)
ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1
unwrapIP :: Type -> CoercionR
unwrapIP ty =
case unwrapNewTyCon_maybe tc of
Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
Nothing -> pprPanic "unwrapIP" $
text "The dictionary for" <+> quotes (ppr tc)
<+> text "is not a newtype!"
where
(tc, tys) = splitTyConApp ty
wrapIP :: Type -> CoercionR
wrapIP ty = mkSymCo (unwrapIP ty)