Moduleghc-10.0.0.20260917GHC2024

GHC.Tc.Types.Evidence

25 types
65 values

Packageghc-10.0.0.20260917
Exports90
LanguageGHC2024
LicenceBSD-3-Clause
SourceEvidence.hs

HsWrapper

23 declarations

datadata HsWrapper

HsWrappers are produced by the typechecker to insert pieces of Core syntax.

For example:

User writes: id False. Typechecker elaborates to id @Bool False using WpTyApp.
User writes: compare True False. Typechecker elaborates to compare $dOrdBool True False using WpEvApp.

A wrapper can be thought of as a function CoreExpr -> CoreExpr which transforms Core syntax by elaboration; we usually write this as expr ↦ wrap[expr]. We often write a wrapper as an "expression with a hole", e.g. WpTyApp Int is hole @Int.

NOTATION ~~>: if wrap[ e::t1 ] :: t2, we write the type of wrap as wrap :: t1 ~~> t2.

Constructors

WpHole
The identity HsWrapper (similar to the Refl coercion).
WpSubType HsWrapper
WpSubType wp is the same as wp, but with extra invariants. See Note Deep subsumption and WpSubType
WpCompose HsWrapper HsWrapper
```
(wrap1 WpCompose wrap2)[e] = wrap1[ wrap2[ e ]]
```
Hence (\a. hole) WpCompose (\b. hole) = (\a b. hole) But (hole a) WpCompose (hole b) = (hole b a)
If wrap1 :: t2 ~> t3 and wrap2 :: t1 ~~> t2, then (wrap1 WpCompose wrap2) :: t1 ~~> t3
WpFun
```
(WpFun mult_co arg_wrap res_wrap t1 t2)[e] = (x :: exp_arg). res_wrap[ e arg_wrap[x] ]
```
INVARIANT: both input and output types of arg_wrap have a fixed runtime-rep See Note [WpFun-FRR-INVARIANT]
Typing rules: given: - mult_co :: act_mult ~ exp_mult - arg_wrap :: exp_arg ~~> act_arg - res_wrap :: act_res ~~> exp_res then WpFun mult_co arg_wrap res_wrap :: (act_arg %act_mult -> arg_res) ~~> (exp_arg %exp_mult -> exp_res).
This isn't the same as for mkFunCo, but it has to be this way because we can't use mkSymCo to flip around these HsWrappers.
NB: a WpFun is always for type-like function arrows; no constraints.
Use mkWpFun to construct such a wrapper.
- mult_co :: SubMultCo
- arg_wrap :: HsWrapper
- res_wrap :: HsWrapper
- arg_type :: TcTypeFRR
  The "from" type of the argument wrapper
- res_type :: TcType
  Either the "from" or the "to" type of the result wrapper
WpCast TcCoercionR
A cast: hole cast co
WpEvLam EvVar
Evidence abstraction d. hole, where d is an evidence variable
WpEvApp EvTerm
hole d, where d@ is evidence for a constraint
WpTyLam TyVar
Type abstraction a. hole, where a is a type/kind variable (not a coercion variable)
WpTyApp KindOrType
Type application hole t, where t is a type/kind (not a coercion)
WpLet TcEvBinds
Evidence bindings: let binds in hole.
The set of evidence bindings should be non-empty (or possibly non-empty), so that the identity HsWrapper is always exactly WpHole.

Instances5Data, Semigroup, Monoid, Outputable, ToHie

Data HsWrapperDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Semigroup HsWrapperDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
The Semigroup instance is a bit fishy, since WpCompose, as a data constructor, is "syntactic" and not associative. Concretely, if a, b, and c aren't WpHole:
```
(a <> b) <> c ?= a <> (b <> c)
```
>
```
(a `WpCompose` b) `WpCompose` c /= @ a `WpCompose` (b `WpCompose` c)
```
However these two associations are are "semantically equal" in the sense that they produce equal functions when passed to GHC.HsToCore.Binds.dsHsWrapper.
Monoid HsWrapperDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable HsWrapperDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
ToHie (LocatedA HsWrapper)Defined in ghc-10.0.0.20260917 · GHC.Iface.Ext.Ast

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

valuemkWpTyApps :: [Type] -> HsWrapper

valuemkWpEvApps :: [EvTerm] -> HsWrapper

valuemkWpEvVarApps :: [EvVar] -> HsWrapper

valuemkWpTyLams :: [TyVar] -> HsWrapper

valuemkWpForAllCast :: [ForAllTyBinder] -> Type -> HsWrapper

valuemkWpEvLams :: [Var] -> HsWrapper

valuemkWpLet :: TcEvBinds -> HsWrapper

valuemkWpFun

:: HsWrapper
-> HsWrapper
-> (SubMultCo, TcTypeFRR)
the "from" type of the first wrapper
-> TcType
Either "from" type or "to" type of the second wrapper (used only when the second wrapper is the identity)
-> HsWrapper

Smart constructor to create a WpFun HsWrapper, which avoids introducing a lambda abstraction if the two supplied wrappers are either identities or casts.

PRECONDITION: same as Note [WpFun-FRR-INVARIANT]

valuemkWpCastN :: TcCoercionN -> HsWrapper

valuemkWpCastR :: TcCoercionR -> HsWrapper

valuemkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper

valuemkWpSubType :: HsWrapper -> HsWrapper

datadata SubMultCo

A sub-multiplicity coercion.

Used only to get multiplicities to line up when typechecking partial applications of data constructors, as per Note [Typechecking data constructors] in GHC.Tc.Gen.Head.

See Note [Multiplicity in deep subsumption]

Constructors

EqMultCo TcCoercionN
Equality of multiplicities
OneSubMult Mult
One is a submultiplicity of any other multiplicity.

Instances2Data, Outputable

Data SubMultCoDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable SubMultCoDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

valuemkSubMultFunCo

:: FunTyFlag
-> FunTyFlag
-> SubMultCo
act_mult ~~> exp_mult
-> TcCoercionR
act_arg ~~> exp_arg
-> TcCoercionR
act_res ~~> exp_res
-> TcCoercionR

Like mkFunCo2 except that it allows for sub-multiplicity instead of a multiplicity coercion.

valuesubMultCoRKind :: SubMultCo -> Mult

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

valueidHsWrapper :: HsWrapper

valueisIdHsWrapper :: HsWrapper -> Bool

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

valuehsWrapDictBinders :: HsWrapper -> Bag DictId

Identifies the lambda-bound dictionaries of an HsWrapper. This is used (only) to allow the pattern-match overlap checker to know what Given dictionaries are in scope.

We specifically do not collect dictionaries bound in a WpLet. These are either superclasses of lambda-bound ones, or (extremely numerous) results of binding Wanted dictionaries. We definitely don't want all those cluttering up the Given dictionaries for pattern-match overlap checking!

valueoptSubTypeHsWrapper :: HsWrapper -> HsWrapper

Evidence bindings

27 declarations

datadata TcEvBinds

Instances3Data, Outputable, ToHie

Data TcEvBindsDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable TcEvBindsDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
ToHie (EvBindContext (LocatedA TcEvBinds))Defined in ghc-10.0.0.20260917 · GHC.Iface.Ext.Ast

datadata EvBindsVar

Constructors

EvBindsVar
- ebv_uniq :: Unique
- ebv_binds :: IORef EvBindsState
CoEvBindsVar
- ebv_uniq :: Unique
- ebv_needs :: IORef NeededEvIds

Instances2Outputable, Uniquable

Outputable EvBindsVarDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Uniquable EvBindsVarDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

typetype NeededEvIds = VarSet

datadata EvBindsState

Constructors

EBS
- ebs_binds :: EvBindsMap
- ebs_needs :: NeededEvIds

Instances1Outputable

Outputable EvBindsStateDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

valueemptyEvBindsState :: EvBindsState

valueunionEvBindsState :: EvBindsState -> EvBindsState -> EvBindsState

valueaddNeededEvIdsEBS :: NeededEvIds -> EvBindsState -> EvBindsState

newtypenewtype EvBindsMap

Constructors

EvBindsMap
- ev_bind_varenv :: DVarEnv EvBind

Instances1Outputable

Outputable EvBindsMapDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

valueemptyEvBindsMap :: EvBindsMap

valueextendEvBinds :: EvBindsMap -> EvBind -> EvBindsMap

valueunionEvBindsMap :: EvBindsMap -> EvBindsMap -> EvBindsMap

Union two evidence binding maps

valuelookupEvBind :: EvBindsMap -> EvVar -> Maybe EvBind

valueevBindMapBinds :: EvBindsMap -> Bag EvBind

valuefoldEvBindsMap :: (EvBind -> a -> a) -> a -> EvBindsMap -> a

valuenonDetStrictFoldEvBindsMap :: (EvBind -> a -> a) -> a -> EvBindsMap -> a

valuefilterEvBindsMap :: (EvBind -> Bool) -> EvBindsMap -> EvBindsMap

valueisEmptyEvBindsMap :: EvBindsMap -> Bool

valueevBindMapToVarSet :: EvBindsMap -> VarSet

valuevarSetMinusEvBindsMap :: VarSet -> EvBindsMap -> VarSet

datadata EvBindInfo

Constructors

EvBindGiven
EvBindWanted
- ebi_canonical :: CanonicalEvidence

datadata EvBind

Constructors

EvBind
- eb_lhs :: EvVar
- eb_rhs :: EvTerm
- eb_info :: EvBindInfo

Instances2Data, Outputable

Data EvBindDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable EvBindDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

valueemptyTcEvBinds :: TcEvBinds

valueisEmptyTcEvBinds :: TcEvBinds -> Bool

valuemkGivenEvBind :: EvVar -> EvTerm -> EvBind

valuemkWantedEvBind :: EvVar -> CanonicalEvidence -> EvTerm -> EvBind

valueevBindVar :: EvBind -> EvVar

valueisCoEvBindsVar :: EvBindsVar -> Bool

EvTerm (already a CoreExpr)

24 declarations

datadata EvTerm

Constructors

EvExpr EvExpr
EvTypeable Type EvTypeable
EvFun
- et_tvs :: [TyVar]
- et_given :: [EvVar]
- et_binds :: TcEvBinds
- et_body :: EvVar

Instances2Data, Outputable

Data EvTermDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable EvTermDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

typetype EvExpr = CoreExpr

valueevId :: EvId -> EvExpr

Any sort of evidence Id, including coercions

valueevCoercion :: TcCoercion -> EvTerm

valueevCast :: EvExpr -> TcCoercion -> EvTerm

valueevCastE :: EvExpr -> TcCoercion -> EvExpr

d |> co

valueevDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm

valueevDictApp :: Class -> [Type] -> [EvExpr] -> EvTerm

valueevSelector :: Id -> [Type] -> [EvExpr] -> EvExpr

valueevDelayedError :: Type -> String -> EvTerm

valuemkEvScSelectors :: Class -> [TcType] -> [(TcPredType, EvExpr)]

valueevTypeable :: Type -> EvTypeable -> EvTerm

valueevWrapIPE :: PredType -> EvExpr -> EvExpr

valueevUnwrapIPE :: PredType -> EvExpr -> EvExpr

valueevUnaryDictAppE :: Class -> [Type] -> EvExpr -> EvExpr

valuemkEvCast :: EvExpr -> TcCoercion -> EvTerm

Deprecated. Please use evCast instead

valuenestedEvIdsOfTerm :: EvTerm -> VarSet

valueevTermFVs :: EvTerm -> SelectiveDFV

valueevTermCoercion :: EvTerm -> TcCoercion

valueevTermCoercion_maybe :: EvTerm -> Maybe TcCoercion

valueevExprCoercion :: EvExpr -> TcCoercion

valueevExprCoercion_maybe :: EvExpr -> Maybe TcCoercion

datadata EvCallStack

Evidence for CallStack implicit parameters.

Constructors

EvCsEmpty
EvCsPushCall FastString RealSrcSpan EvExpr
EvCsPushCall origin loc stk represents a call from origin, occurring at loc, in a calling context stk.

Instances2Data, Outputable

Data EvCallStackDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable EvCallStackDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

datadata 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 EvTerm
Dictionary for Typeable (s % w -> t), given a dictionaries for w, 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 #10348)

Instances2Data, Outputable

Data EvTypeableDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable EvTypeableDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

HoleExprRef

1 declaration

datadata HoleExprRef

Where to store evidence for expression holes See Note [Holes in expressions] in GHC.Hs.Expr.

Constructors

HER (IORef EvTerm) TcType Unique

Instances2Data, Outputable

Data HoleExprRefDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence
Outputable HoleExprRefDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

TcCoercion

12 declarations

typetype TcCoercion = Coercion

typetype TcCoercionR = CoercionR

typetype TcCoercionN = CoercionN

typetype TcCoercionP = CoercionP

datadata CoercionHole

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

Instances3Data, Outputable, Uniquable

Data CoercionHoleDefined in ghc-10.0.0.20260917 · GHC.Core.TyCo.Rep
Outputable CoercionHoleDefined in ghc-10.0.0.20260917 · GHC.Core.TyCo.Rep
Uniquable CoercionHoleDefined in ghc-10.0.0.20260917 · GHC.Core.TyCo.Rep

typetype TcMCoercion = MCoercion

typetype TcMCoercionN = MCoercionN

typetype TcMCoercionR = MCoercionR

datadata Role

See Note [Roles] in GHC.Core.Coercion

Order of constructors matters: the Ord instance coincides with the *super*typing relation on roles.

Nominal Representational Phantom

Instances7Eq, Data, Ord, NFData, Outputable, Binary, …

Eq RoleDefined in ghc-10.0.0.20260917 · Language.Haskell.Syntax.Basic
Data RoleDefined in ghc-10.0.0.20260917 · Language.Haskell.Syntax.Basic
Ord RoleDefined in ghc-10.0.0.20260917 · Language.Haskell.Syntax.Basic
NFData RoleDefined in ghc-10.0.0.20260917 · GHC.Core.Coercion.Axiom · orphan
Outputable RoleDefined in ghc-10.0.0.20260917 · GHC.Core.Coercion.Axiom · orphan
Binary RoleDefined in ghc-10.0.0.20260917 · GHC.Core.Coercion.Axiom · orphan
type Anno (Maybe Role) = EpAnnCODefined in ghc-10.0.0.20260917 · GHC.Hs.Decls · orphan

datadata LeftOrRight

CLeft CRight

Instances6Eq, Data, Ord, NFData, Outputable, Binary

Eq LeftOrRightDefined in ghc-10.0.0.20260917 · GHC.Types.Basic
Data LeftOrRightDefined in ghc-10.0.0.20260917 · GHC.Types.Basic
Ord LeftOrRightDefined in ghc-10.0.0.20260917 · GHC.Types.Basic
NFData LeftOrRightDefined in ghc-10.0.0.20260917 · GHC.Types.Basic
Outputable LeftOrRightDefined in ghc-10.0.0.20260917 · GHC.Types.Basic
Binary LeftOrRightDefined in ghc-10.0.0.20260917 · GHC.Types.Basic

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

valuemaybeSymCo :: SwapFlag -> TcCoercion -> TcCoercion

If a SwapFlag is IsSwapped, flip the orientation of a coercion

QuoteWrapper

3 declarations

datadata QuoteWrapper

Constructors

QuoteWrapper EvVar Type

Instances1Data

Data QuoteWrapperDefined in ghc-10.0.0.20260917 · GHC.Tc.Types.Evidence

valueapplyQuoteWrapper :: QuoteWrapper -> HsWrapper

Convert the QuoteWrapper into a normal HsWrapper which can be used to apply its contents.

valuequoteWrapperTyVarTy :: QuoteWrapper -> Type