ghc-9.8.1: The GHC API
Safe HaskellNone
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

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]

isTopLevelUserTypeError :: PredType -> Bool Source #

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

containsUserTypeError :: PredType -> Bool Source #

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

isUnsatisfiableCt_maybe :: Type -> Maybe ErrorMsgType Source #

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

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 #

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

Constructors

EqCt 

Instances

Instances details
Outputable EqCt Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: EqCt -> SDoc Source #

data DictCt Source #

Constructors

DictCt 

Instances

Instances details
Outputable DictCt Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: DictCt -> SDoc Source #

data IrredCt Source #

Constructors

IrredCt 

Instances

Instances details
Outputable IrredCt Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: IrredCt -> SDoc Source #

data QCInst Source #

Instances

Instances details
Outputable QCInst Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: QCInst -> SDoc Source #

type ExpansionFuel = Int Source #

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

doNotExpand :: ExpansionFuel Source #

Do not expand superclasses any further

consumeFuel :: ExpansionFuel -> ExpansionFuel Source #

Consumes one unit of fuel. Precondition: fuel > 0

pendingFuel :: ExpansionFuel -> Bool Source #

Returns True if we have any fuel left for superclass expansion

assertFuelPrecondition :: ExpansionFuel -> a -> a Source #

asserts if fuel is non-negative

assertFuelPreconditionStrict :: ExpansionFuel -> a -> a Source #

asserts if fuel is strictly greater than 0

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

PluginReason

A typechecker plugin returned this in the pluginBadCts field of TcPluginProgress

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

Instances

Instances details
Outputable CheckTyEqProblem Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

Eq CheckTyEqProblem Source # 
Instance details

Defined in GHC.Tc.Types.Constraint

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

    TyCon of the family

  • [Xi]

    Arguments, 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 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

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

Local typechecker environment for a constraint.

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

See also TcLclCtxt.

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 #

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.

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

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

eqCtFlavourRole :: EqCt -> CtFlavourRole Source #

Extract the flavour and role from a Ct