module GHC.Tc.Types.Evidence (
HsWrapper(..),
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
mkWpFun, idHsWrapper, isIdHsWrapper,
pprHsWrapper, hsWrapDictBinders,
TcEvBinds(..), EvBindsVar(..),
EvBindMap(..), emptyEvBindMap, extendEvBinds,
lookupEvBind, evBindMapBinds,
foldEvBindMap, nonDetStrictFoldEvBindMap,
filterEvBindMap,
isEmptyEvBindMap,
evBindMapToVarSet,
varSetMinusEvBindMap,
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,
TcMCoercion,
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,
mkTcCoVarCo,
mkTcFamilyTyConAppCo,
isTcReflCo, isTcReflexiveCo,
tcCoercionRole,
unwrapIP, wrapIP,
QuoteWrapper(..), applyQuoteWrapper, quoteWrapperTyVarTy
) where
#include "HsVersions.h"
import GHC.Prelude
import GHC.Types.Unique.DFM
import GHC.Types.Unique.FM
import GHC.Types.Var
import GHC.Core.Coercion.Axiom
import GHC.Core.Coercion
import GHC.Core.Ppr ()
import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.DataCon( DataCon, dataConWrapId )
import GHC.Core.Class( Class )
import GHC.Builtin.Names
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Core.Predicate
import GHC.Types.Name
import GHC.Data.Pair
import GHC.Core
import GHC.Core.Class ( classSCSelId )
import GHC.Core.FVs ( exprSomeFreeVars )
import GHC.Utils.Misc
import GHC.Data.Bag
import qualified Data.Data as Data
import GHC.Utils.Outputable
import GHC.Types.SrcLoc
import Data.IORef( IORef )
import GHC.Types.Unique.Set
import GHC.Core.Multiplicity
type TcCoercion = Coercion
type TcCoercionN = CoercionN
type TcCoercionR = CoercionR
type TcCoercionP = CoercionP
type TcMCoercion = MCoercion
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 -> 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
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
mkTcFamilyTyConAppCo :: TyCon -> [TcCoercionN] -> TcCoercionN
tcCoercionKind :: TcCoercion -> Pair TcType
tcCoercionRole :: TcCoercion -> Role
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
tcDowngradeRole = downgradeRole
mkTcAxiomRuleCo = mkAxiomRuleCo
mkTcGReflRightCo = mkGReflRightCo
mkTcGReflLeftCo = mkGReflLeftCo
mkTcCoherenceLeftCo = mkCoherenceLeftCo
mkTcCoherenceRightCo = mkCoherenceRightCo
mkTcPhantomCo = mkPhantomCo
mkTcKindCo = mkKindCo
mkTcCoVarCo = mkCoVarCo
mkTcFamilyTyConAppCo = mkFamilyTyConAppCo
tcCoercionKind = coercionKind
tcCoercionRole = coercionRole
isTcReflCo = isReflCo
isTcReflexiveCo = isReflexiveCo
maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
maybeTcSubCo NomEq = id
maybeTcSubCo ReprEq = mkTcSubCo
data HsWrapper
= WpHole
| WpCompose HsWrapper HsWrapper
| WpFun HsWrapper HsWrapper (Scaled TcType) SDoc
| WpCast TcCoercionR
| WpEvLam EvVar
| WpEvApp EvTerm
| WpTyLam TyVar
| WpTyApp KindOrType
| WpLet TcEvBinds
| WpMultCoercion Coercion
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
gfoldl k z (WpMultCoercion a1) = z WpMultCoercion `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)
9 -> k (z WpLet)
_ -> k (z WpMultCoercion)
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
toConstr (WpMultCoercion _) = wpMultCoercion_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, wpMultCoercion_constr ]
wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr,
wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr,
wpMultCoercion_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"
wpMultCoercion_constr = mkHsWrapperConstr "WpMultCoercion"
mkHsWrapperConstr :: String -> Data.Constr
mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix
wpFunEmpty :: HsWrapper -> HsWrapper -> Scaled 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
-> (Scaled TcType)
-> TcType
-> SDoc
-> HsWrapper
mkWpFun WpHole WpHole _ _ _ = WpHole
mkWpFun WpHole (WpCast co2) (Scaled w t1) _ _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2)
mkWpFun (WpCast co1) WpHole (Scaled w _) t2 _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2))
mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2)
mkWpFun co1 co2 t1 _ d = WpFun co1 co2 t1 d
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
hsWrapDictBinders :: HsWrapper -> Bag DictId
hsWrapDictBinders wrap = go wrap
where
go (WpEvLam dict_id) = unitBag dict_id
go (w1 `WpCompose` w2) = go w1 `unionBags` go w2
go (WpFun _ w _ _) = go w
go WpHole = emptyBag
go (WpCast {}) = emptyBag
go (WpEvApp {}) = emptyBag
go (WpTyLam {}) = emptyBag
go (WpTyApp {}) = emptyBag
go (WpLet {}) = emptyBag
go (WpMultCoercion {}) = emptyBag
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)
nonDetStrictFoldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
nonDetStrictFoldEvBindMap k z bs = nonDetStrictFoldDVarEnv 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 }
evBindMapToVarSet :: EvBindMap -> VarSet
evBindMapToVarSet (EvBindMap dve) = unsafeUFMToUniqSet (mapUFM evBindVar (udfmToUfm dve))
varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet
varSetMinusEvBindMap vs (EvBindMap dve) = vs `uniqSetMinusUDFM` dve
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 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 = nonDetStrictFoldUniqSet 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 em e1 e2 -> evVarsOfTerms [em,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
= sdocOption sdocPrintTypecheckerElaboration $ \case
True -> help pp_thing_inside wrap False
False -> 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 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> 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]
help it (WpMultCoercion co) = add_parens $ sep [it False, nest 2 (text "<multiplicity coercion>"
<+> pprParendCo co)]
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 tm t1 t2) = parens (ppr t1 <+> mulArrow (ppr tm) <+> 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)
data QuoteWrapper = QuoteWrapper EvVar Type deriving Data.Data
quoteWrapperTyVarTy :: QuoteWrapper -> Type
quoteWrapperTyVarTy (QuoteWrapper _ t) = t
applyQuoteWrapper :: QuoteWrapper -> HsWrapper
applyQuoteWrapper (QuoteWrapper ev_var m_var)
= mkWpEvVarApps [ev_var] <.> mkWpTyApps [m_var]