GHC.Tc.Types.Constraint

This module defines types and simple operations over constraints, as used in the type-checker and constraint solver.

Documentation

type Xi = TcType

A Xi-type is one that has been fully rewritten with respect to the inert set; that is, it has been rewritten by the algorithm in GHC.Tc.Solver.Rewrite. (Historical note: Xi, for years and years, meant that a type was type-family-free. It does *not* mean this any more.)

data Ct

Constructors

CDictCan DictCt

CIrredCan IrredCt

CEqCan EqCt

CQuantCan QCInst

CNonCanonical CtEvidence

Instances

Outputable Ct

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Ct -> SDoc

type Cts = Bag Ct

singleCt :: Ct -> Cts

listToCts :: [Ct] -> Cts

ctsElts :: Cts -> [Ct]

consCts :: Ct -> Cts -> Cts

snocCts :: Cts -> Ct -> Cts

extendCtsList :: Cts -> [Ct] -> Cts

isEmptyCts :: Cts -> Bool

emptyCts :: Cts

andCts :: Cts -> Cts -> Cts

ctsPreds :: Cts -> [PredType]

isPendingScDictCt :: DictCt -> Bool

isPendingScDict :: Ct -> Bool

pendingScDict_maybe :: Ct -> Maybe Ct

superClassesMightHelp :: WantedConstraints -> Bool

True if taking superclasses of givens, or of wanteds (to perhaps expose more equalities or functional dependencies) might help to solve this constraint. See Note [When superclasses help]

getPendingWantedScs :: Cts -> ([Ct], Cts)

isWantedCt :: Ct -> Bool

isGivenCt :: Ct -> Bool

isTopLevelUserTypeError :: PredType -> Bool

Is this an user error message type, i.e. either the form TypeError err or Unsatisfiable err?

containsUserTypeError :: PredType -> Bool

Does this constraint contain an user error message?

That is, the type is either of the form Unsatisfiable err, or it contains a type of the form TypeError msg, either at the top level or nested inside the type.

getUserTypeErrorMsg :: PredType -> Maybe ErrorMsgType

A constraint is considered to be a custom type error, if it contains custom type errors anywhere in it. See Note [Custom type errors in constraints]

isUnsatisfiableCt_maybe :: Type -> Maybe ErrorMsgType

Is this type an unsatisfiable constraint? If so, return the error message.

ctEvidence :: Ct -> CtEvidence

updCtEvidence :: (CtEvidence -> CtEvidence) -> Ct -> Ct

ctLoc :: Ct -> CtLoc

ctPred :: Ct -> PredType

ctFlavour :: Ct -> CtFlavour

Get the flavour of the given Ct

ctEqRel :: Ct -> EqRel

Get the equality relation for the given Ct

ctOrigin :: Ct -> CtOrigin

ctRewriters :: Ct -> RewriterSet

ctEvId :: HasDebugCallStack => Ct -> EvVar

wantedEvId_maybe :: Ct -> Maybe EvVar

Returns the evidence Id for the argument Ct when this Ct is a Wanted.

Returns Nothing otherwise.

mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType

Makes a new equality predicate with the same role as the given evidence.

mkNonCanonical :: CtEvidence -> Ct

mkGivens :: CtLoc -> [EvId] -> [Ct]

tyCoVarsOfCt :: Ct -> TcTyCoVarSet

Returns free variables of constraints as a non-deterministic set

tyCoVarsOfCts :: Cts -> TcTyCoVarSet

Returns free variables of a bag of constraints as a non-deterministic set. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfCtList :: Ct -> [TcTyCoVar]

Returns free variables of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]

Returns free variables of a bag of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

data EqCt

Constructors

EqCt

Fields

• eq_ev :: CtEvidence
• eq_lhs :: CanEqLHS
• eq_rhs :: Xi
• eq_eq_rel :: EqRel

Instances

Outputable EqCt

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: EqCt -> SDoc

eqCtEvidence :: EqCt -> CtEvidence

eqCtLHS :: EqCt -> CanEqLHS

data DictCt

Constructors

DictCt

Fields

• di_ev :: CtEvidence
• di_cls :: Class
• di_tys :: [Xi]
• di_pend_sc :: ExpansionFuel

Instances

Outputable DictCt

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: DictCt -> SDoc

dictCtEvidence :: DictCt -> CtEvidence

data IrredCt

Constructors

IrredCt

Fields

• ir_ev :: CtEvidence
• ir_reason :: CtIrredReason

Instances

Outputable IrredCt

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: IrredCt -> SDoc

irredCtEvidence :: IrredCt -> CtEvidence

mkIrredCt :: CtIrredReason -> CtEvidence -> Ct

ctIrredCt :: CtIrredReason -> Ct -> IrredCt

irredCtPred :: IrredCt -> PredType

data QCInst

Constructors

QCI

Fields

• qci_ev :: CtEvidence
• qci_tvs :: [TcTyVar]
• qci_pred :: TcPredType
• qci_pend_sc :: ExpansionFuel

Instances

Outputable QCInst

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: QCInst -> SDoc

pendingScInst_maybe :: QCInst -> Maybe QCInst

type ExpansionFuel = Int

Says how many layers of superclasses can we expand. Invariant: ExpansionFuel should always be >= 0 see Note [Expanding Recursive Superclasses and ExpansionFuel]

doNotExpand :: ExpansionFuel

Do not expand superclasses any further

consumeFuel :: ExpansionFuel -> ExpansionFuel

Consumes one unit of fuel. Precondition: fuel > 0

pendingFuel :: ExpansionFuel -> Bool

Returns True if we have any fuel left for superclass expansion

assertFuelPrecondition :: ExpansionFuel -> a -> a

asserts if fuel is non-negative

assertFuelPreconditionStrict :: ExpansionFuel -> a -> a

asserts if fuel is strictly greater than 0

data CtIrredReason

Used to indicate extra information about why a CIrredCan is irreducible

Constructors

IrredShapeReason

This constraint has a non-canonical shape (e.g. c Int, for a variable c)

NonCanonicalReason CheckTyEqResult

An equality where some invariant other than (TyEq:H) of CEqCan is not satisfied; the CheckTyEqResult states exactly why

ReprEqReason

An equality that cannot be decomposed because it is representational. Example: a b ~R# Int. These might still be solved later. INVARIANT: The constraint is a representational equality constraint

ShapeMismatchReason

A nominal equality that relates two wholly different types, like Int ~# Bool or a b ~# 3. INVARIANT: The constraint is a nominal equality constraint

AbstractTyConReason

An equality like T a b c ~ Q d e where either T or Q is an abstract type constructor. See Note [Skolem abstract data] in GHC.Core.TyCon. INVARIANT: The constraint is an equality constraint between two TyConApps

PluginReason

A typechecker plugin returned this in the pluginBadCts field of TcPluginProgress

Instances

Outputable CtIrredReason

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtIrredReason -> SDoc

isInsolubleReason :: CtIrredReason -> Bool

Are we sure that more solving will never solve this constraint?

data CheckTyEqResult

A set of problems in checking the validity of a type equality. See checkTypeEq.

Instances

Monoid CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: CheckTyEqResult

mappend :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult

mconcat :: [CheckTyEqResult] -> CheckTyEqResult

Semigroup CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

(<>) :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult

sconcat :: NonEmpty CheckTyEqResult -> CheckTyEqResult

stimes :: Integral b => b -> CheckTyEqResult -> CheckTyEqResult

Outputable CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CheckTyEqResult -> SDoc

data CheckTyEqProblem

An individual problem that might be logged in a CheckTyEqResult

Instances

Outputable CheckTyEqProblem

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CheckTyEqProblem -> SDoc

Eq CheckTyEqProblem

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: CheckTyEqProblem -> CheckTyEqProblem -> Bool

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

cteProblem :: CheckTyEqProblem -> CheckTyEqResult

cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult

cteOK :: CheckTyEqResult

No problems in checking the validity of a type equality.

cteImpredicative :: CheckTyEqProblem

cteTypeFamily :: CheckTyEqProblem

cteCoercionHole :: CheckTyEqProblem

cteInsolubleOccurs :: CheckTyEqProblem

cteSolubleOccurs :: CheckTyEqProblem

cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult

Mark a CheckTyEqResult as not having an insoluble occurs-check: any occurs check under a type family or in a representation equality is soluble.

cteConcrete :: CheckTyEqProblem

cteSkolemEscape :: CheckTyEqProblem

impredicativeProblem :: CheckTyEqResult

insolubleOccursProblem :: CheckTyEqResult

solubleOccursProblem :: CheckTyEqResult

cterHasNoProblem :: CheckTyEqResult -> Bool

Check whether a CheckTyEqResult is marked successful.

cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool

Check whether a CheckTyEqResult has a CheckTyEqProblem

cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool

Check whether a CheckTyEqResult has one CheckTyEqProblem and no other

cterHasOnlyProblems :: CheckTyEqResult -> CheckTyEqResult -> Bool

cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult

cterHasOccursCheck :: CheckTyEqResult -> Bool

cterFromKind :: CheckTyEqResult -> CheckTyEqResult

Retain only information about occurs-check failures, because only that matters after recurring into a kind.

data CanEqLHS

A CanEqLHS is a type that can appear on the left of a canonical equality: a type variable or exactly-saturated type family application.

Constructors

TyVarLHS TcTyVar

TyFamLHS

Fields

• TyCon

  TyCon of the family

• [Xi]

  Arguments, exactly saturating the family

Instances

Outputable CanEqLHS

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CanEqLHS -> SDoc

canEqLHS_maybe :: Xi -> Maybe CanEqLHS

Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated type family application? Does not look through type synonyms.

canTyFamEqLHS_maybe :: Xi -> Maybe CanEqLHS

canEqLHSKind :: CanEqLHS -> TcKind

Retrieve the kind of a CanEqLHS

canEqLHSType :: CanEqLHS -> TcType

Convert a CanEqLHS back into a Type

eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool

Are two CanEqLHSs equal?

data Hole

A hole stores the information needed to report diagnostics about holes in terms (unbound identifiers or underscores) or in types (also called wildcards, as used in partial type signatures). See Note [Holes].

Constructors

Hole

Fields

• hole_sort :: HoleSort

  What flavour of hole is this?

• hole_occ :: RdrName

  The name of this hole

• hole_ty :: TcType

  Type to be printed to the user For expression holes: type of expr For type holes: the missing type

• hole_loc :: CtLoc

  Where hole was written

Instances

Outputable Hole

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Hole -> SDoc

data HoleSort

Used to indicate which sort of hole we have.

Constructors

ExprHole HoleExprRef

Either an out-of-scope variable or a "true" hole in an expression (TypedHoles). The HoleExprRef says where to write the the erroring expression for -fdefer-type-errors.

TypeHole

A hole in a type (PartialTypeSignatures)

ConstraintHole

A hole in a constraint, like @f :: (_, Eq a) => ... Differentiated from TypeHole because a ConstraintHole is simplified differently. See Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.

Instances

Outputable HoleSort

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: HoleSort -> SDoc

isOutOfScopeHole :: Hole -> Bool

Does this hole represent an "out of scope" error? See Note [Insoluble holes]

data DelayedError

A delayed error, to be reported after constraint solving, in order to benefit from deferred unifications.

Constructors

DE_Hole Hole

A hole (in a type or in a term).

See Note [Holes].

DE_NotConcrete NotConcreteError

A type could not be ensured to be concrete.

See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.

Instances

Outputable DelayedError

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: DelayedError -> SDoc

data NotConcreteError

Why did we require that a certain type be concrete?

Constructors

NCE_FRR

Concreteness was required by a representation-polymorphism check.

See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.

Fields

• nce_loc :: CtLoc

  Where did this check take place?

• nce_frr_origin :: FixedRuntimeRepOrigin

  Which representation-polymorphism check did we perform?

• nce_reasons :: NonEmpty NotConcreteReason

  Why did the check fail?

Instances

Outputable NotConcreteError

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: NotConcreteError -> SDoc

data NotConcreteReason

Why did we decide that a type was not concrete?

Constructors

NonConcreteTyCon TyCon [TcType]

The type contains a TyConApp of a non-concrete TyCon.

See Note [Concrete types] in GHC.Tc.Utils.Concrete.

NonConcretisableTyVar TyVar

The type contains a type variable that could not be made concrete (e.g. a skolem type variable).

ContainsCast TcType TcCoercionN

The type contains a cast.

ContainsForall ForAllTyBinder TcType

The type contains a forall.

ContainsCoercionTy TcCoercion

The type contains a CoercionTy.

data WantedConstraints

Constructors

WC

Fields

• wc_simple :: Cts
• wc_impl :: Bag Implication
• wc_errors :: Bag DelayedError

Instances

Outputable WantedConstraints

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: WantedConstraints -> SDoc

insolubleWC :: WantedConstraints -> Bool

emptyWC :: WantedConstraints

isEmptyWC :: WantedConstraints -> Bool

isSolvedWC :: WantedConstraints -> Bool

Checks whether a the given wanted constraints are solved, i.e. that there are no simple constraints left and all the implications are solved.

andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints

unionsWC :: [WantedConstraints] -> WantedConstraints

mkSimpleWC :: [CtEvidence] -> WantedConstraints

mkImplicWC :: Bag Implication -> WantedConstraints

addInsols :: WantedConstraints -> Bag IrredCt -> WantedConstraints

dropMisleading :: WantedConstraints -> WantedConstraints

addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints

addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints

addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints

addNotConcreteError :: WantedConstraints -> NotConcreteError -> WantedConstraints

addDelayedErrors :: WantedConstraints -> Bag DelayedError -> WantedConstraints

tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet

Returns free variables of WantedConstraints as a non-deterministic set. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]

Returns free variables of WantedConstraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

insolubleWantedCt :: Ct -> Bool

insolubleCt :: Ct -> Bool

Returns True of constraints that are definitely insoluble, as well as TypeError constraints. Can return True for Given constraints, unlike insolubleWantedCt.

The function is tuned for application after constraint solving i.e. assuming canonicalisation has been done That's why it looks only for IrredCt; all insoluble constraints are put into CIrredCan

insolubleIrredCt :: IrredCt -> Bool

insolubleImplic :: Implication -> Bool

nonDefaultableTyVarsOfWC :: WantedConstraints -> TyCoVarSet

Gather all the type variables from WantedConstraints that it would be unhelpful to default. For the moment, these are only ConcreteTv metavariables participating in a nominal equality whose other side is not concrete; it's usually better to report those as errors instead of defaulting.

data Implication

Constructors

Implic

Fields

• ic_tclvl :: TcLevel
• ic_info :: SkolemInfoAnon
• ic_skols :: [TcTyVar]
• ic_given :: [EvVar]
• ic_given_eqs :: HasGivenEqs
• ic_warn_inaccessible :: Bool
• ic_env :: !CtLocEnv
• ic_wanted :: WantedConstraints
• ic_binds :: EvBindsVar
• ic_need_inner :: VarSet
• ic_need_outer :: VarSet
• ic_status :: ImplicStatus

Instances

Outputable Implication

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Implication -> SDoc

implicationPrototype :: CtLocEnv -> Implication

checkTelescopeSkol :: SkolemInfoAnon -> Bool

data ImplicStatus

Constructors

IC_Solved

Fields

• ics_dead :: [EvVar]

IC_Insoluble

IC_BadTelescope

IC_Unsolved

Instances

Outputable ImplicStatus

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: ImplicStatus -> SDoc

isInsolubleStatus :: ImplicStatus -> Bool

isSolvedStatus :: ImplicStatus -> Bool

type UserGiven = Implication

getUserGivensFromImplics :: [Implication] -> [UserGiven]

data HasGivenEqs

Constructors

NoGivenEqs

LocalGivenEqs

MaybeGivenEqs

Instances

Monoid HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: HasGivenEqs

mappend :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs

mconcat :: [HasGivenEqs] -> HasGivenEqs

Semigroup HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

(<>) :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs

sconcat :: NonEmpty HasGivenEqs -> HasGivenEqs

stimes :: Integral b => b -> HasGivenEqs -> HasGivenEqs

Outputable HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: HasGivenEqs -> SDoc

Eq HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: HasGivenEqs -> HasGivenEqs -> Bool

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

checkImplicationInvariants :: (HasCallStack, Applicative m) => Implication -> m ()

data SubGoalDepth

See Note [SubGoalDepth]

Instances

Outputable SubGoalDepth

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: SubGoalDepth -> SDoc

Eq SubGoalDepth

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: SubGoalDepth -> SubGoalDepth -> Bool

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

Ord SubGoalDepth

Defined in GHC.Tc.Types.Constraint

Methods

compare :: SubGoalDepth -> SubGoalDepth -> Ordering

(<) :: SubGoalDepth -> SubGoalDepth -> Bool

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

(>) :: SubGoalDepth -> SubGoalDepth -> Bool

(>=) :: SubGoalDepth -> SubGoalDepth -> Bool

max :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth

min :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth

initialSubGoalDepth :: SubGoalDepth

maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth

bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth

subGoalDepthExceeded :: IntWithInf -> SubGoalDepth -> Bool

data CtLoc

Constructors

CtLoc

Fields

• ctl_origin :: CtOrigin
• ctl_env :: CtLocEnv
• ctl_t_or_k :: Maybe TypeOrKind
• ctl_depth :: !SubGoalDepth

ctLocSpan :: CtLoc -> RealSrcSpan

ctLocEnv :: CtLoc -> CtLocEnv

ctLocLevel :: CtLoc -> TcLevel

ctLocOrigin :: CtLoc -> CtOrigin

ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind

ctLocDepth :: CtLoc -> SubGoalDepth

bumpCtLocDepth :: CtLoc -> CtLoc

isGivenLoc :: CtLoc -> Bool

setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc

updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc

setCtLocEnv :: CtLoc -> CtLocEnv -> CtLoc

setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc

pprCtLoc :: CtLoc -> SDoc

adjustCtLoc :: Bool -> Bool -> CtLoc -> CtLoc

adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc

data CtLocEnv

Local typechecker environment for a constraint.

Used to restore the environment of a constraint when reporting errors, see setCtLocM.

See also TcLclCtxt.

Constructors

CtLocEnv

Fields

• ctl_ctxt :: ![ErrCtxt]
• ctl_loc :: !RealSrcSpan
• ctl_bndrs :: !TcBinderStack
• ctl_tclvl :: !TcLevel
• ctl_in_gen_code :: !Bool
• ctl_rdr :: !LocalRdrEnv

setCtLocEnvLoc :: CtLocEnv -> SrcSpan -> CtLocEnv

setCtLocEnvLvl :: CtLocEnv -> TcLevel -> CtLocEnv

getCtLocEnvLoc :: CtLocEnv -> RealSrcSpan

getCtLocEnvLvl :: CtLocEnv -> TcLevel

ctLocEnvInGeneratedCode :: CtLocEnv -> Bool

data CtEvidence

Constructors

CtGiven

Fields

• ctev_pred :: TcPredType
• ctev_evar :: EvVar
• ctev_loc :: CtLoc

CtWanted

Fields

• ctev_pred :: TcPredType
• ctev_dest :: TcEvDest
• ctev_loc :: CtLoc
• ctev_rewriters :: RewriterSet

Instances

Outputable CtEvidence

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtEvidence -> SDoc

data TcEvDest

A place for type-checking evidence to go after it is generated.

• Wanted equalities use HoleDest,
• other Wanteds use EvVarDest.

Constructors

EvVarDest EvVar

bind this var to the evidence EvVarDest is always used for non-type-equalities e.g. class constraints

HoleDest CoercionHole

fill in this hole with the evidence HoleDest is always used for type-equalities See Note [Coercion holes] in GHC.Core.TyCo.Rep

Instances

Outputable TcEvDest

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: TcEvDest -> SDoc

isWanted :: CtEvidence -> Bool

isGiven :: CtEvidence -> Bool

ctEvPred :: CtEvidence -> TcPredType

ctEvLoc :: CtEvidence -> CtLoc

ctEvOrigin :: CtEvidence -> CtOrigin

ctEvEqRel :: CtEvidence -> EqRel

Get the equality relation relevant for a CtEvidence

ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr

ctEvTerm :: CtEvidence -> EvTerm

ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion

ctEvEvId :: CtEvidence -> EvVar

ctEvRewriters :: CtEvidence -> RewriterSet

Extract the set of rewriters from a CtEvidence See Note [Wanteds rewrite Wanteds] If the provided CtEvidence is not for a Wanted, just return an empty set.

ctEvUnique :: CtEvidence -> Unique

tcEvDestUnique :: TcEvDest -> Unique

mkKindEqLoc :: TcType -> TcType -> CtLoc -> CtLoc

toKindLoc :: CtLoc -> CtLoc

Take a CtLoc and moves it to the kind level

toInvisibleLoc :: CtLoc -> CtLoc

mkGivenLoc :: TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc

ctEvRole :: CtEvidence -> Role

Get the role relevant for a CtEvidence

setCtEvPredType :: HasDebugCallStack => CtEvidence -> Type -> CtEvidence

Set the type of CtEvidence.

This function ensures that the invariants on CtEvidence hold, by updating the evidence and the ctev_pred in sync with each other. See Note [CtEvidence invariants].

setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence

arisesFromGivens :: Ct -> Bool

tyCoVarsOfCtEvList :: CtEvidence -> [TcTyCoVar]

Returns free variables of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

tyCoVarsOfCtEv :: CtEvidence -> TcTyCoVarSet

Returns free variables of constraints as a non-deterministic set

tyCoVarsOfCtEvsList :: [CtEvidence] -> [TcTyCoVar]

Returns free variables of a bag of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.

newtype RewriterSet

Stores a set of CoercionHoles that have been used to rewrite a constraint. See Note [Wanteds rewrite Wanteds].

Constructors

RewriterSet (UniqSet CoercionHole)

Instances

Monoid RewriterSet

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: RewriterSet

mappend :: RewriterSet -> RewriterSet -> RewriterSet

mconcat :: [RewriterSet] -> RewriterSet

Semigroup RewriterSet

Defined in GHC.Tc.Types.Constraint

Methods

(<>) :: RewriterSet -> RewriterSet -> RewriterSet

sconcat :: NonEmpty RewriterSet -> RewriterSet

stimes :: Integral b => b -> RewriterSet -> RewriterSet

Outputable RewriterSet

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: RewriterSet -> SDoc

emptyRewriterSet :: RewriterSet

isEmptyRewriterSet :: RewriterSet -> Bool

addRewriter :: RewriterSet -> CoercionHole -> RewriterSet

unitRewriterSet :: CoercionHole -> RewriterSet

unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet

rewriterSetFromCts :: Bag Ct -> RewriterSet

wrapType :: Type -> [TyVar] -> [PredType] -> Type

data CtFlavour

Constructors

Given

Wanted

Instances

Outputable CtFlavour

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtFlavour -> SDoc

Eq CtFlavour

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: CtFlavour -> CtFlavour -> Bool

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

ctEvFlavour :: CtEvidence -> CtFlavour

type CtFlavourRole = (CtFlavour, EqRel)

Whether or not one Ct can rewrite another is determined by its flavour and its equality relation. See also Note [Flavours with roles] in GHC.Tc.Solver.InertSet

ctEvFlavourRole :: CtEvidence -> CtFlavourRole

Extract the flavour, role, and boxity from a CtEvidence

ctFlavourRole :: Ct -> CtFlavourRole

Extract the flavour and role from a Ct

eqCtFlavourRole :: EqCt -> CtFlavourRole

Extract the flavour and role from a Ct

eqCanRewrite :: EqRel -> EqRel -> Bool

eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool

pprEvVarTheta :: [EvVar] -> SDoc

pprEvVars :: [EvVar] -> SDoc

pprEvVarWithType :: EvVar -> SDoc