TcEvidence

Documentation

data HsWrapper

Constructors

WpHole

WpCompose HsWrapper HsWrapper

WpFun HsWrapper HsWrapper TcType SDoc

WpCast TcCoercionR

WpEvLam EvVar

WpEvApp EvTerm

WpTyLam TyVar

WpTyApp KindOrType

WpLet TcEvBinds

Instances

Data HsWrapper

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HsWrapper

toConstr :: HsWrapper -> Constr

dataTypeOf :: HsWrapper -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HsWrapper)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper)

gmapT :: (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r

gmapQ :: (forall d. Data d => d -> u) -> HsWrapper -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HsWrapper -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper

Outputable HsWrapper

Defined in TcEvidence

Methods

ppr :: HsWrapper -> SDoc

pprPrec :: Rational -> HsWrapper -> SDoc

(<.>) :: HsWrapper -> HsWrapper -> HsWrapper

mkWpTyApps :: [Type] -> HsWrapper

mkWpEvApps :: [EvTerm] -> HsWrapper

mkWpEvVarApps :: [EvVar] -> HsWrapper

mkWpTyLams :: [TyVar] -> HsWrapper

mkWpLams :: [Var] -> HsWrapper

mkWpLet :: TcEvBinds -> HsWrapper

mkWpCastN :: TcCoercionN -> HsWrapper

mkWpCastR :: TcCoercionR -> HsWrapper

collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)

mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> SDoc -> HsWrapper

mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper

mkWpFuns [(ty1, wrap1), (ty2, wrap2)] ty_res wrap_res, where wrap1 :: ty1 "->" ty1' and wrap2 :: ty2 "->" ty2', wrap3 :: ty3 "->" ty3' and ty_res is either ty3 or ty3', gives a wrapper (ty1' -> ty2' -> ty3) "->" (ty1 -> ty2 -> ty3'). Notice that the result wrapper goes the other way round to all the others. This is a result of sub-typing contravariance. The SDoc is a description of what you were doing when you called mkWpFuns.

idHsWrapper :: HsWrapper

isIdHsWrapper :: HsWrapper -> Bool

pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc

data TcEvBinds

Constructors

TcEvBinds EvBindsVar

EvBinds (Bag EvBind)

Instances

Data TcEvBinds

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TcEvBinds -> c TcEvBinds

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TcEvBinds

toConstr :: TcEvBinds -> Constr

dataTypeOf :: TcEvBinds -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TcEvBinds)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TcEvBinds)

gmapT :: (forall b. Data b => b -> b) -> TcEvBinds -> TcEvBinds

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TcEvBinds -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TcEvBinds -> r

gmapQ :: (forall d. Data d => d -> u) -> TcEvBinds -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TcEvBinds -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds

Outputable TcEvBinds

Defined in TcEvidence

Methods

ppr :: TcEvBinds -> SDoc

pprPrec :: Rational -> TcEvBinds -> SDoc

data EvBindsVar

Constructors

EvBindsVar

Fields

• ebv_uniq :: Unique
• ebv_binds :: IORef EvBindMap
• ebv_tcvs :: IORef CoVarSet

Instances

Outputable EvBindsVar

Defined in TcEvidence

Methods

ppr :: EvBindsVar -> SDoc

pprPrec :: Rational -> EvBindsVar -> SDoc

Uniquable EvBindsVar

Defined in TcEvidence

Methods

getUnique :: EvBindsVar -> Unique

newtype EvBindMap

Constructors

EvBindMap

Fields

• ev_bind_varenv :: DVarEnv EvBind

Instances

Outputable EvBindMap

Defined in TcEvidence

Methods

ppr :: EvBindMap -> SDoc

pprPrec :: Rational -> EvBindMap -> SDoc

emptyEvBindMap :: EvBindMap

extendEvBinds :: EvBindMap -> EvBind -> EvBindMap

lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind

evBindMapBinds :: EvBindMap -> Bag EvBind

foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a

filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap

isEmptyEvBindMap :: EvBindMap -> Bool

data EvBind

Constructors

EvBind

Fields

• eb_lhs :: EvVar
• eb_rhs :: EvTerm
• eb_is_given :: Bool

Instances

Outputable EvBind

Defined in TcEvidence

Methods

ppr :: EvBind -> SDoc

pprPrec :: Rational -> EvBind -> SDoc

emptyTcEvBinds :: TcEvBinds

isEmptyTcEvBinds :: TcEvBinds -> Bool

mkGivenEvBind :: EvVar -> EvTerm -> EvBind

mkWantedEvBind :: EvVar -> EvTerm -> EvBind

sccEvBinds :: Bag EvBind -> [SCC EvBind]

Do SCC analysis on a bag of EvBinds.

evBindVar :: EvBind -> EvVar

data EvTerm

Constructors

EvId EvId

EvCoercion TcCoercion

EvCast EvTerm TcCoercionR

EvDFunApp DFunId [Type] [EvTerm]

EvDelayedError Type FastString

EvSuperClass EvTerm Int

EvLit EvLit

EvCallStack EvCallStack

EvTypeable Type EvTypeable

EvSelector Id [Type] [EvTerm]

Instances

Data EvTerm

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvTerm -> c EvTerm

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvTerm

toConstr :: EvTerm -> Constr

dataTypeOf :: EvTerm -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvTerm)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)

gmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r

gmapQ :: (forall d. Data d => d -> u) -> EvTerm -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EvTerm -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm

Outputable EvTerm

Defined in TcEvidence

Methods

ppr :: EvTerm -> SDoc

pprPrec :: Rational -> EvTerm -> SDoc

mkEvCast :: EvTerm -> TcCoercion -> EvTerm

evVarsOfTerm :: EvTerm -> VarSet

mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]

data EvLit

Constructors

EvNum Integer

EvStr FastString

Instances

Data EvLit

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvLit -> c EvLit

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvLit

toConstr :: EvLit -> Constr

dataTypeOf :: EvLit -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvLit)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvLit)

gmapT :: (forall b. Data b => b -> b) -> EvLit -> EvLit

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvLit -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvLit -> r

gmapQ :: (forall d. Data d => d -> u) -> EvLit -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EvLit -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvLit -> m EvLit

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvLit -> m EvLit

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvLit -> m EvLit

Outputable EvLit

Defined in TcEvidence

Methods

ppr :: EvLit -> SDoc

pprPrec :: Rational -> EvLit -> SDoc

evTermCoercion :: EvTerm -> TcCoercion

data EvCallStack

Evidence for CallStack implicit parameters.

Constructors

EvCsEmpty

EvCsPushCall Name RealSrcSpan EvTerm

EvCsPushCall name loc stk represents a call to name, occurring at loc, in a calling context stk.

Instances

Data EvCallStack

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvCallStack

toConstr :: EvCallStack -> Constr

dataTypeOf :: EvCallStack -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvCallStack)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvCallStack)

gmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r

gmapQ :: (forall d. Data d => d -> u) -> EvCallStack -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EvCallStack -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack

Outputable EvCallStack

Defined in TcEvidence

Methods

ppr :: EvCallStack -> SDoc

pprPrec :: Rational -> EvCallStack -> SDoc

data EvTypeable

Instructions on how to make a Typeable dictionary. See Note [Typeable evidence terms]

Constructors

EvTypeableTyCon TyCon [EvTerm]

Dictionary for Typeable T where T is a type constructor with all of its kind variables saturated. The [EvTerm] is Typeable evidence for the applied kinds..

EvTypeableTyApp EvTerm EvTerm

Dictionary for Typeable (s t), given a dictionaries for s and t.

EvTypeableTrFun EvTerm EvTerm

Dictionary for Typeable (s -> t), given a dictionaries for s and t.

EvTypeableTyLit EvTerm

Dictionary for a type literal, e.g. Typeable "foo" or Typeable 3 The EvTerm is evidence of, e.g., KnownNat 3 (see Trac #10348)

Instances

Data EvTypeable

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvTypeable

toConstr :: EvTypeable -> Constr

dataTypeOf :: EvTypeable -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvTypeable)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)

gmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r

gmapQ :: (forall d. Data d => d -> u) -> EvTypeable -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EvTypeable -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable

Outputable EvTypeable

Defined in TcEvidence

Methods

ppr :: EvTypeable -> SDoc

pprPrec :: Rational -> EvTypeable -> SDoc

type TcCoercion = Coercion

type TcCoercionR = CoercionR

type TcCoercionN = CoercionN

type TcCoercionP = CoercionP

data CoercionHole

A coercion to be filled in by the type-checker. See Note [Coercion holes]

Instances

Data CoercionHole

Defined in TyCoRep

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoercionHole -> c CoercionHole

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoercionHole

toConstr :: CoercionHole -> Constr

dataTypeOf :: CoercionHole -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoercionHole)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoercionHole)

gmapT :: (forall b. Data b => b -> b) -> CoercionHole -> CoercionHole

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r

gmapQ :: (forall d. Data d => d -> u) -> CoercionHole -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CoercionHole -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole

Outputable CoercionHole

Defined in TyCoRep

Methods

ppr :: CoercionHole -> SDoc

pprPrec :: Rational -> CoercionHole -> SDoc

data Role

Constructors

Nominal

Representational

Phantom

Instances

Eq Role

Defined in CoAxiom

Methods

(==) :: Role -> Role -> Bool

(/=) :: Role -> Role -> Bool

Data Role

Defined in CoAxiom

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role

toConstr :: Role -> Constr

dataTypeOf :: Role -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role)

gmapT :: (forall b. Data b => b -> b) -> Role -> Role

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r

gmapQ :: (forall d. Data d => d -> u) -> Role -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role

Ord Role

Defined in CoAxiom

Methods

compare :: Role -> Role -> Ordering

(<) :: Role -> Role -> Bool

(<=) :: Role -> Role -> Bool

(>) :: Role -> Role -> Bool

(>=) :: Role -> Role -> Bool

max :: Role -> Role -> Role

min :: Role -> Role -> Role

Outputable Role

Defined in CoAxiom

Methods

ppr :: Role -> SDoc

pprPrec :: Rational -> Role -> SDoc

Binary Role

Defined in CoAxiom

Methods

put_ :: BinHandle -> Role -> IO ()

put :: BinHandle -> Role -> IO (Bin Role)

get :: BinHandle -> IO Role

data LeftOrRight

Constructors

CLeft

CRight

Instances

Eq LeftOrRight

Defined in BasicTypes

Methods

(==) :: LeftOrRight -> LeftOrRight -> Bool

(/=) :: LeftOrRight -> LeftOrRight -> Bool

Data LeftOrRight

Defined in BasicTypes

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LeftOrRight -> c LeftOrRight

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LeftOrRight

toConstr :: LeftOrRight -> Constr

dataTypeOf :: LeftOrRight -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LeftOrRight)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LeftOrRight)

gmapT :: (forall b. Data b => b -> b) -> LeftOrRight -> LeftOrRight

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r

gmapQ :: (forall d. Data d => d -> u) -> LeftOrRight -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LeftOrRight -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

Outputable LeftOrRight

Defined in BasicTypes

Methods

ppr :: LeftOrRight -> SDoc

pprPrec :: Rational -> LeftOrRight -> SDoc

Binary LeftOrRight

Defined in Binary

Methods

put_ :: BinHandle -> LeftOrRight -> IO ()

put :: BinHandle -> LeftOrRight -> IO (Bin LeftOrRight)

get :: BinHandle -> IO LeftOrRight

pickLR :: LeftOrRight -> (a, a) -> a

mkTcReflCo :: Role -> TcType -> 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

mkTcSymCo :: TcCoercion -> TcCoercion

mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion

mkTcNthCo :: Int -> TcCoercion -> TcCoercion

mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion

mkTcSubCo :: TcCoercionN -> TcCoercionR

maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion

tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion

mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR

mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion

mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion

mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP

mkTcKindCo :: TcCoercion -> TcCoercionN

tcCoercionKind :: TcCoercion -> Pair TcType

coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet

mkTcCoVarCo :: CoVar -> TcCoercion

isTcReflCo :: TcCoercion -> Bool

isTcReflexiveCo :: TcCoercion -> Bool

This version does a slow check, calculating the related types and seeing if they are equal.

tcCoercionRole :: TcCoercion -> Role

unwrapIP :: Type -> CoercionR

Create a Coercion that unwraps an implicit-parameter or overloaded-label dictionary to expose the underlying value. We expect the Type to have the form `IP sym ty` or `IsLabel sym ty`, and return a Coercion `co :: IP sym ty ~ ty` or `co :: IsLabel sym ty ~ Proxy# sym -> ty`. See also Note [Type-checking overloaded labels] in TcExpr.

wrapIP :: Type -> CoercionR

Create a Coercion that wraps a value in an implicit-parameter dictionary. See unwrapIP.