ghc-9.6.0.20230128: The GHC API
Safe HaskellSafe-Inferred
LanguageHaskell2010

GHC.Tc.Types.Constraint

Description

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

Synopsis

Documentation

data QCInst Source #

Constructors

QCI 

Instances

Instances details
Outputable QCInst Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: QCInst -> SDoc Source #

type Xi = TcType Source #

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 Source #

Instances

Instances details
Outputable Ct Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Ct -> SDoc Source #

type Cts = Bag Ct Source #

superClassesMightHelp :: WantedConstraints -> Bool Source #

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]

getUserTypeErrorMsg :: PredType -> Maybe Type Source #

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]

ctFlavour :: Ct -> CtFlavour Source #

Get the flavour of the given Ct

ctEqRel :: Ct -> EqRel Source #

Get the equality relation for the given Ct

wantedEvId_maybe :: Ct -> Maybe EvVar Source #

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

Returns Nothing otherwise.

mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType Source #

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

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

ctEvEqRel :: CtEvidence -> EqRel Source #

Get the equality relation relevant for a CtEvidence

ctEvRewriters :: CtEvidence -> RewriterSet Source #

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.

tyCoVarsOfCt :: Ct -> TcTyCoVarSet Source #

Returns free variables of constraints as a non-deterministic set

tyCoVarsOfCts :: Cts -> TcTyCoVarSet Source #

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

tyCoVarsOfCtList :: Ct -> [TcTyCoVar] Source #

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

tyCoVarsOfCtsList :: Cts -> [TcTyCoVar] Source #

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

data CtIrredReason Source #

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

Instances

Instances details
Outputable CtIrredReason Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

isInsolubleReason :: CtIrredReason -> Bool Source #

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

data CheckTyEqProblem Source #

An individual problem that might be logged in a CheckTyEqResult

cteOK :: CheckTyEqResult Source #

No problems in checking the validity of a type equality.

cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult Source #

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

cterHasNoProblem :: CheckTyEqResult -> Bool Source #

Check whether a CheckTyEqResult is marked successful.

cterFromKind :: CheckTyEqResult -> CheckTyEqResult Source #

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

data CanEqLHS Source #

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

    of the family

  • [Xi]

    exactly saturating the family

Instances

Instances details
Outputable CanEqLHS Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CanEqLHS -> SDoc Source #

canEqLHS_maybe :: Xi -> Maybe CanEqLHS Source #

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.

canEqLHSKind :: CanEqLHS -> TcKind Source #

Retrieve the kind of a CanEqLHS

canEqLHSType :: CanEqLHS -> TcType Source #

Convert a CanEqLHS back into a Type

eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool Source #

Are two CanEqLHSs equal?

data Hole Source #

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

Instances

Instances details
Outputable Hole Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Hole -> SDoc Source #

data HoleSort Source #

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

Instances details
Outputable HoleSort Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: HoleSort -> SDoc Source #

isOutOfScopeHole :: Hole -> Bool Source #

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

data DelayedError Source #

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

Instances details
Outputable DelayedError Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

data NotConcreteError Source #

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

Instances

Instances details
Outputable NotConcreteError Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

data NotConcreteReason Source #

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 Source #

Constructors

WC 

Instances

Instances details
Outputable WantedConstraints Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

isSolvedWC :: WantedConstraints -> Bool Source #

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

tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet Source #

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

tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar] Source #

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

insolubleCt :: Ct -> Bool Source #

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

nonDefaultableTyVarsOfWC :: WantedConstraints -> TyCoVarSet Source #

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 ImplicStatus Source #

Instances

Instances details
Outputable ImplicStatus Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

data CtEvidence Source #

Instances

Instances details
Outputable CtEvidence Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtEvidence -> SDoc Source #

data TcEvDest Source #

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

Instances details
Outputable TcEvDest Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: TcEvDest -> SDoc Source #

toKindLoc :: CtLoc -> CtLoc Source #

Take a CtLoc and moves it to the kind level

ctEvRole :: CtEvidence -> Role Source #

Get the role relevant for a CtEvidence

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

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

tyCoVarsOfCtEvList :: CtEvidence -> [TcTyCoVar] Source #

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

tyCoVarsOfCtEv :: CtEvidence -> TcTyCoVarSet Source #

Returns free variables of constraints as a non-deterministic set

tyCoVarsOfCtEvsList :: [CtEvidence] -> [TcTyCoVar] Source #

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

newtype RewriterSet Source #

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

rewriterSetFromType :: Type -> RewriterSet Source #

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

rewriterSetFromTypes :: [Type] -> RewriterSet Source #

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

rewriterSetFromCo :: Coercion -> RewriterSet Source #

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

data CtFlavour Source #

Constructors

Given 
Wanted 

Instances

Instances details
Outputable CtFlavour Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtFlavour -> SDoc Source #

Eq CtFlavour Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

type CtFlavourRole = (CtFlavour, EqRel) Source #

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 Source #

Extract the flavour, role, and boxity from a CtEvidence

ctFlavourRole :: Ct -> CtFlavourRole Source #

Extract the flavour and role from a Ct