GHC.Tc.Types.Constraint

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

Documentation

data QCInst

Constructors

QCI

Fields

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

Instances

Outputable QCInst

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: QCInst -> SDoc

isPendingScInst :: QCInst -> Maybe QCInst

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

Fields

• cc_ev :: CtEvidence
• cc_class :: Class
• cc_tyargs :: [Xi]
• cc_pend_sc :: Bool

CIrredCan

Fields

• cc_ev :: CtEvidence
• cc_reason :: CtIrredReason

CEqCan

Fields

• cc_ev :: CtEvidence
• cc_lhs :: CanEqLHS
• cc_rhs :: Xi
• cc_eq_rel :: EqRel

CNonCanonical

Fields

• cc_ev :: CtEvidence

CQuantCan QCInst

Instances

Outputable Ct

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: Ct -> SDoc

type Cts = Bag Ct

emptyCts :: Cts

andCts :: Cts -> Cts -> Cts

andManyCts :: [Cts] -> Cts

pprCts :: Cts -> SDoc

singleCt :: Ct -> Cts

listToCts :: [Ct] -> Cts

ctsElts :: Cts -> [Ct]

consCts :: Ct -> Cts -> Cts

snocCts :: Cts -> Ct -> Cts

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

isEmptyCts :: Cts -> Bool

isPendingScDict :: 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

isDerivedCt :: Ct -> Bool

isGivenCt :: Ct -> Bool

isUserTypeErrorCt :: Ct -> Bool

getUserTypeErrorMsg :: Ct -> Maybe Type

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]

ctEvidence :: Ct -> CtEvidence

ctLoc :: Ct -> CtLoc

setCtLoc :: Ct -> CtLoc -> Ct

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

ctEvId :: Ct -> EvVar

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

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

mkNonCanonical :: CtEvidence -> Ct

mkNonCanonicalCt :: Ct -> Ct

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

mkIrredCt :: CtIrredReason -> CtEvidence -> Ct

ctEvPred :: CtEvidence -> TcPredType

ctEvLoc :: CtEvidence -> CtLoc

ctEvOrigin :: CtEvidence -> CtOrigin

ctEvEqRel :: CtEvidence -> EqRel

Get the equality relation relevant for a CtEvidence

ctEvExpr :: CtEvidence -> EvExpr

ctEvTerm :: CtEvidence -> EvTerm

ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion

ctEvEvId :: CtEvidence -> EvVar

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

HoleBlockerReason HoleSet

this constraint is blocked on the coercion hole(s) listed See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical Wrinkle (4a). Why store the HoleSet? See Wrinkle (2) of that same Note. INVARIANT: A HoleBlockerReason constraint is a homogeneous equality whose left hand side can fit in a CanEqLHS.

NonCanonicalReason CheckTyEqResult

an equality where some invariant other than (TyEq:H) of CEqCan is not satisfied; the CheckTyEqResult states exactly why INVARIANT: the CheckTyEqResult has some bit set other than cteHoleBlocker

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

Outputable CtIrredReason

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtIrredReason -> SDoc

type HoleSet = UniqSet CoercionHole

A set of CoercionHoles

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

Semigroup CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

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

sconcat :: NonEmpty CheckTyEqResult -> CheckTyEqResult

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

Monoid CheckTyEqResult

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: CheckTyEqResult

mappend :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult

mconcat :: [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

cteProblem :: CheckTyEqProblem -> CheckTyEqResult

cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult

cteOK :: CheckTyEqResult

No problems in checking the validity of a type equality.

cteImpredicative :: CheckTyEqProblem

cteTypeFamily :: CheckTyEqProblem

cteHoleBlocker :: 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.

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

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

  of the family

• [Xi]

  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.

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 :: OccName

  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 WantedConstraints

Constructors

WC

Fields

• wc_simple :: Cts
• wc_impl :: Bag Implication
• wc_holes :: Bag Hole

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 Ct -> WantedConstraints

dropMisleading :: WantedConstraints -> WantedConstraints

addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints

addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints

addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints

tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet

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

dropDerivedWC :: WantedConstraints -> WantedConstraints

dropDerivedSimples :: Cts -> Cts

tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]

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

insolubleCt :: Ct -> Bool

insolubleEqCt :: Ct -> Bool

isDroppableCt :: Ct -> Bool

insolubleImplic :: Implication -> Bool

arisesFromGivens :: Ct -> Bool

data Implication

Constructors

Implic

Fields

• ic_tclvl :: TcLevel
• ic_skols :: [TcTyVar]
• ic_info :: SkolemInfo
• ic_given :: [EvVar]
• ic_given_eqs :: HasGivenEqs
• ic_warn_inaccessible :: Bool
• ic_env :: TcLclEnv
• 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 :: Implication

checkTelescopeSkol :: SkolemInfo -> 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

data HasGivenEqs

Constructors

NoGivenEqs

LocalGivenEqs

MaybeGivenEqs

Instances

Eq HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

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

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

Semigroup HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

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

sconcat :: NonEmpty HasGivenEqs -> HasGivenEqs

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

Monoid HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

mempty :: HasGivenEqs

mappend :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs

mconcat :: [HasGivenEqs] -> HasGivenEqs

Outputable HasGivenEqs

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: HasGivenEqs -> SDoc

data SubGoalDepth

See Note [SubGoalDepth]

Instances

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

Outputable SubGoalDepth

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: SubGoalDepth -> SDoc

initialSubGoalDepth :: SubGoalDepth

maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth

bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth

subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool

data CtLoc

Constructors

CtLoc

Fields

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

ctLocSpan :: CtLoc -> RealSrcSpan

ctLocEnv :: CtLoc -> TcLclEnv

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 -> TcLclEnv -> CtLoc

setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc

pprCtLoc :: CtLoc -> SDoc

data CtEvidence

Constructors

CtGiven

Fields

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

CtWanted

Fields

• ctev_pred :: TcPredType
• ctev_dest :: TcEvDest
• ctev_nosh :: ShadowInfo
• ctev_loc :: CtLoc

CtDerived

Fields

• ctev_pred :: TcPredType
• ctev_loc :: CtLoc

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 are always HoleDest; other wanteds are always 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

mkKindLoc :: TcType -> TcType -> CtLoc -> CtLoc

toKindLoc :: CtLoc -> CtLoc

Take a CtLoc and moves it to the kind level

mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc

isWanted :: CtEvidence -> Bool

isGiven :: CtEvidence -> Bool

isDerived :: CtEvidence -> Bool

ctEvRole :: CtEvidence -> Role

Get the role relevant for a CtEvidence

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

data CtFlavour

Constructors

Given

Wanted ShadowInfo

Derived

Instances

Eq CtFlavour

Defined in GHC.Tc.Types.Constraint

Methods

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

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

Outputable CtFlavour

Defined in GHC.Tc.Types.Constraint

Methods

ppr :: CtFlavour -> SDoc

data ShadowInfo

Constructors

WDeriv

WOnly

Instances

Eq ShadowInfo

Defined in GHC.Tc.Types.Constraint

Methods

(==) :: ShadowInfo -> ShadowInfo -> Bool

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

ctFlavourContainsDerived :: CtFlavour -> Bool

Does this CtFlavour subsumed Derived? True of [WD] and [D].

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

ctEvFlavourRole :: CtEvidence -> CtFlavourRole

Extract the flavour, role, and boxity from a CtEvidence

ctFlavourRole :: Ct -> CtFlavourRole

Extract the flavour and role from a Ct

eqCanRewrite :: EqRel -> EqRel -> Bool

eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool

eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool

eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool

pprEvVarTheta :: [EvVar] -> SDoc

pprEvVars :: [EvVar] -> SDoc

pprEvVarWithType :: EvVar -> SDoc