GHC.Tc.Types.Constraint

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.)

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]

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]

Get the flavour of the given Ct

Get the equality relation for the given Ct

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

Returns Nothing otherwise.

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

Get the equality relation relevant for a CtEvidence

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.

Returns free variables of constraints as a non-deterministic set

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

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

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

Used to indicate extra information about why a CIrredCan is irreducible

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

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

An individual problem that might be logged in a CheckTyEqResult

No problems in checking the validity of a type equality.

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

Check whether a CheckTyEqResult is marked successful.

Check whether a CheckTyEqResult has a CheckTyEqProblem

Check whether a CheckTyEqResult has one CheckTyEqProblem and no other

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

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

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.

Retrieve the kind of a CanEqLHS

Convert a CanEqLHS back into a Expr

Are two CanEqLHSs equal?

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].

Used to indicate which sort of hole we have.

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

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

Why did we require that a certain type be concrete?

Why did we decide that a type was not concrete?

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

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

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

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

This function is critical for accurate pattern-match overlap warnings. See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver

Note that this does not traverse through the constraint to find nested custom type errors: it only detects TypeError msg :: Constraint, and not e.g. Eq (TypeError msg).

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.

See Note [SubGoalDepth]

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

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

Take a CtLoc and moves it to the kind level

Get the role relevant for a 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].

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

Returns free variables of constraints as a non-deterministic set

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

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

Makes a RewriterSet from all the coercion holes that occur in the given type.

Makes a RewriterSet from all the coercion holes that occur in the given types.

Makes a RewriterSet from all the coercion holes that occur in the given coercion.

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

Extract the flavour, role, and boxity from a CtEvidence

Extract the flavour and role from a Ct