Safe Haskell	Safe-Inferred
Language	Haskell2010

GHC.Tc.Types.Constraint

Description

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

Synopsis

data QCInst = QCI {
- qci_ev :: CtEvidence
- qci_tvs :: [TcTyVar]
- qci_pred :: TcPredType
- qci_pend_sc :: Bool
}
pendingScInst_maybe :: QCInst -> Maybe QCInst
type Xi = TcType
data Ct
- = CDictCan {
  - cc_ev :: CtEvidence
  - cc_class :: Class
  - cc_tyargs :: [Xi]
  - cc_pend_sc :: Bool
  }
- | CIrredCan {
  - cc_ev :: CtEvidence
  - cc_reason :: CtIrredReason
  }
- | CEqCan {
  - cc_ev :: CtEvidence
  - cc_lhs :: CanEqLHS
  - cc_rhs :: Xi
  - cc_eq_rel :: EqRel
  }
- | CNonCanonical {
  - cc_ev :: CtEvidence
  }
- | CQuantCan QCInst
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 -> Bool
pendingScDict_maybe :: Ct -> Maybe Ct
superClassesMightHelp :: WantedConstraints -> Bool
getPendingWantedScs :: Cts -> ([Ct], Cts)
isWantedCt :: Ct -> Bool
isGivenCt :: Ct -> Bool
isUserTypeError :: PredType -> Bool
getUserTypeErrorMsg :: PredType -> Maybe Type
ctEvidence :: Ct -> CtEvidence
ctLoc :: Ct -> CtLoc
ctPred :: Ct -> PredType
ctFlavour :: Ct -> CtFlavour
ctEqRel :: Ct -> EqRel
ctOrigin :: Ct -> CtOrigin
ctRewriters :: Ct -> RewriterSet
ctEvId :: HasDebugCallStack => Ct -> EvVar
wantedEvId_maybe :: Ct -> Maybe EvVar
mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
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
ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr
ctEvTerm :: CtEvidence -> EvTerm
ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion
ctEvEvId :: CtEvidence -> EvVar
ctEvRewriters :: CtEvidence -> RewriterSet
tyCoVarsOfCt :: Ct -> TcTyCoVarSet
tyCoVarsOfCts :: Cts -> TcTyCoVarSet
tyCoVarsOfCtList :: Ct -> [TcTyCoVar]
tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]
data CtIrredReason
- = IrredShapeReason
- | NonCanonicalReason CheckTyEqResult
- | ReprEqReason
- | ShapeMismatchReason
- | AbstractTyConReason
isInsolubleReason :: CtIrredReason -> Bool
data CheckTyEqResult
data CheckTyEqProblem
cteProblem :: CheckTyEqProblem -> CheckTyEqResult
cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult
cteOK :: CheckTyEqResult
cteImpredicative :: CheckTyEqProblem
cteTypeFamily :: CheckTyEqProblem
cteInsolubleOccurs :: CheckTyEqProblem
cteSolubleOccurs :: CheckTyEqProblem
cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult
cterHasNoProblem :: CheckTyEqResult -> Bool
cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
cterHasOccursCheck :: CheckTyEqResult -> Bool
cterFromKind :: CheckTyEqResult -> CheckTyEqResult
data CanEqLHS
- = TyVarLHS TcTyVar
- | TyFamLHS TyCon [Xi]
canEqLHS_maybe :: Xi -> Maybe CanEqLHS
canEqLHSKind :: CanEqLHS -> TcKind
canEqLHSType :: CanEqLHS -> TcType
eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
data Hole = Hole {
- hole_sort :: HoleSort
- hole_occ :: RdrName
- hole_ty :: TcType
- hole_loc :: CtLoc
}
data HoleSort
- = ExprHole HoleExprRef
- | TypeHole
- | ConstraintHole
isOutOfScopeHole :: Hole -> Bool
data DelayedError
- = DE_Hole Hole
- | DE_NotConcrete NotConcreteError
data NotConcreteError = NCE_FRR {
- nce_loc :: CtLoc
- nce_frr_origin :: FixedRuntimeRepOrigin
- nce_reasons :: NonEmpty NotConcreteReason
}
data NotConcreteReason
- = NonConcreteTyCon TyCon [TcType]
- | NonConcretisableTyVar TyVar
- | ContainsCast TcType TcCoercionN
- | ContainsForall ForAllTyBinder TcType
- | ContainsCoercionTy TcCoercion
data WantedConstraints = WC {
- wc_simple :: Cts
- wc_impl :: Bag Implication
- wc_errors :: Bag DelayedError
}
insolubleWC :: WantedConstraints -> Bool
emptyWC :: WantedConstraints
isEmptyWC :: WantedConstraints -> Bool
isSolvedWC :: WantedConstraints -> Bool
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
addNotConcreteError :: WantedConstraints -> NotConcreteError -> WantedConstraints
addDelayedErrors :: WantedConstraints -> Bag DelayedError -> WantedConstraints
tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]
insolubleWantedCt :: Ct -> Bool
insolubleEqCt :: Ct -> Bool
insolubleCt :: Ct -> Bool
insolubleImplic :: Implication -> Bool
nonDefaultableTyVarsOfWC :: WantedConstraints -> TyCoVarSet
data Implication = Implic {
- ic_tclvl :: TcLevel
- ic_info :: SkolemInfoAnon
- ic_skols :: [TcTyVar]
- 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
}
implicationPrototype :: Implication
checkTelescopeSkol :: SkolemInfoAnon -> Bool
data ImplicStatus
- = IC_Solved {
  - ics_dead :: [EvVar]
  }
- | IC_Insoluble
- | IC_BadTelescope
- | IC_Unsolved
isInsolubleStatus :: ImplicStatus -> Bool
isSolvedStatus :: ImplicStatus -> Bool
type UserGiven = Implication
getUserGivensFromImplics :: [Implication] -> [UserGiven]
data HasGivenEqs
- = NoGivenEqs
- | LocalGivenEqs
- | MaybeGivenEqs
checkImplicationInvariants :: (HasCallStack, Applicative m) => Implication -> m ()
data SubGoalDepth
initialSubGoalDepth :: SubGoalDepth
maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
data CtLoc = CtLoc {
- 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
- = CtGiven {
  - ctev_pred :: TcPredType
  - ctev_evar :: EvVar
  - ctev_loc :: CtLoc
  }
- | CtWanted {
  - ctev_pred :: TcPredType
  - ctev_dest :: TcEvDest
  - ctev_loc :: CtLoc
  - ctev_rewriters :: RewriterSet
  }
data TcEvDest
- = EvVarDest EvVar
- | HoleDest CoercionHole
mkKindLoc :: TcType -> TcType -> CtLoc -> CtLoc
toKindLoc :: CtLoc -> CtLoc
mkGivenLoc :: TcLevel -> SkolemInfoAnon -> TcLclEnv -> CtLoc
isWanted :: CtEvidence -> Bool
isGiven :: CtEvidence -> Bool
ctEvRole :: CtEvidence -> Role
setCtEvPredType :: HasDebugCallStack => CtEvidence -> Type -> CtEvidence
setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence
tyCoVarsOfCtEvList :: CtEvidence -> [TcTyCoVar]
tyCoVarsOfCtEv :: CtEvidence -> TcTyCoVarSet
tyCoVarsOfCtEvsList :: [CtEvidence] -> [TcTyCoVar]
ctEvUnique :: CtEvidence -> Unique
tcEvDestUnique :: TcEvDest -> Unique
newtype RewriterSet = RewriterSet (UniqSet CoercionHole)
emptyRewriterSet :: RewriterSet
isEmptyRewriterSet :: RewriterSet -> Bool
rewriterSetFromType :: Type -> RewriterSet
rewriterSetFromTypes :: [Type] -> RewriterSet
rewriterSetFromCo :: Coercion -> RewriterSet
addRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet
wrapType :: Type -> [TyVar] -> [PredType] -> Type
data CtFlavour
- = Given
- | Wanted
ctEvFlavour :: CtEvidence -> CtFlavour
type CtFlavourRole = (CtFlavour, EqRel)
ctEvFlavourRole :: CtEvidence -> CtFlavourRole
ctFlavourRole :: Ct -> CtFlavourRole
eqCanRewrite :: EqRel -> EqRel -> Bool
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
pprEvVarTheta :: [EvVar] -> SDoc
pprEvVars :: [EvVar] -> SDoc
pprEvVarWithType :: EvVar -> SDoc

Documentation

data QCInst Source #

Constructors

QCI
Fields qci_ev :: CtEvidence qci_tvs :: [TcTyVar] qci_pred :: TcPredType qci_pend_sc :: Bool

Instances

Instances details

Outputable QCInst Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: QCInst -> SDoc Source #

pendingScInst_maybe :: QCInst -> Maybe QCInst 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 #

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

Instances details

Outputable Ct Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: Ct -> SDoc Source #

type Cts = Bag Ct Source #

emptyCts :: Cts Source #

andCts :: Cts -> Cts -> Cts Source #

andManyCts :: [Cts] -> Cts Source #

pprCts :: Cts -> SDoc Source #

singleCt :: Ct -> Cts Source #

listToCts :: [Ct] -> Cts Source #

ctsElts :: Cts -> [Ct] Source #

consCts :: Ct -> Cts -> Cts Source #

snocCts :: Cts -> Ct -> Cts Source #

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

isEmptyCts :: Cts -> Bool Source #

isPendingScDict :: Ct -> Bool Source #

pendingScDict_maybe :: Ct -> Maybe 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]

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

isWantedCt :: Ct -> Bool Source #

isGivenCt :: Ct -> Bool Source #

isUserTypeError :: PredType -> Bool Source #

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]

ctEvidence :: Ct -> CtEvidence Source #

ctLoc :: Ct -> CtLoc Source #

ctPred :: Ct -> PredType Source #

ctFlavour :: Ct -> CtFlavour Source #

Get the flavour of the given Ct

ctEqRel :: Ct -> EqRel Source #

Get the equality relation for the given Ct

ctOrigin :: Ct -> CtOrigin Source #

ctRewriters :: Ct -> RewriterSet Source #

ctEvId :: HasDebugCallStack => Ct -> EvVar Source #

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.

mkNonCanonical :: CtEvidence -> Ct Source #

mkNonCanonicalCt :: Ct -> Ct Source #

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

mkIrredCt :: CtIrredReason -> CtEvidence -> Ct Source #

ctEvPred :: CtEvidence -> TcPredType Source #

ctEvLoc :: CtEvidence -> CtLoc Source #

ctEvOrigin :: CtEvidence -> CtOrigin Source #

ctEvEqRel :: CtEvidence -> EqRel Source #

Get the equality relation relevant for a CtEvidence

ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr Source #

ctEvTerm :: CtEvidence -> EvTerm Source #

ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion Source #

ctEvEvId :: CtEvidence -> EvVar Source #

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 Methods ppr :: CtIrredReason -> SDoc Source #

isInsolubleReason :: CtIrredReason -> Bool Source #

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

data CheckTyEqResult Source #

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

Instances

Instances details

Monoid CheckTyEqResult Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods mempty :: CheckTyEqResult Source # mappend :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult Source # mconcat :: [CheckTyEqResult] -> CheckTyEqResult Source #
Semigroup CheckTyEqResult Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods (<>) :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult Source # sconcat :: NonEmpty CheckTyEqResult -> CheckTyEqResult Source # stimes :: Integral b => b -> CheckTyEqResult -> CheckTyEqResult Source #
Outputable CheckTyEqResult Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: CheckTyEqResult -> SDoc Source #

data CheckTyEqProblem Source #

An individual problem that might be logged in a CheckTyEqResult

cteProblem :: CheckTyEqProblem -> CheckTyEqResult Source #

cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult Source #

cteOK :: CheckTyEqResult Source #

No problems in checking the validity of a type equality.

cteImpredicative :: CheckTyEqProblem Source #

cteTypeFamily :: CheckTyEqProblem Source #

cteInsolubleOccurs :: CheckTyEqProblem Source #

cteSolubleOccurs :: CheckTyEqProblem Source #

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.

cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool Source #

Check whether a CheckTyEqResult has a CheckTyEqProblem

cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool Source #

Check whether a CheckTyEqResult has one CheckTyEqProblem and no other

cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult Source #

cterHasOccursCheck :: CheckTyEqResult -> Bool Source #

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

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 #

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

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 Methods ppr :: DelayedError -> SDoc Source #

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

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

Instances details

Outputable NotConcreteError Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: NotConcreteError -> SDoc Source #

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
Fields wc_simple :: Cts wc_impl :: Bag Implication wc_errors :: Bag DelayedError

Instances

Instances details

Outputable WantedConstraints Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: WantedConstraints -> SDoc Source #

insolubleWC :: WantedConstraints -> Bool Source #

emptyWC :: WantedConstraints Source #

isEmptyWC :: WantedConstraints -> Bool Source #

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.

andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints Source #

unionsWC :: [WantedConstraints] -> WantedConstraints Source #

mkSimpleWC :: [CtEvidence] -> WantedConstraints Source #

mkImplicWC :: Bag Implication -> WantedConstraints Source #

addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints Source #

dropMisleading :: WantedConstraints -> WantedConstraints Source #

addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints Source #

addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints Source #

addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints Source #

addNotConcreteError :: WantedConstraints -> NotConcreteError -> WantedConstraints Source #

addDelayedErrors :: WantedConstraints -> Bag DelayedError -> WantedConstraints Source #

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.

insolubleWantedCt :: Ct -> Bool Source #

insolubleEqCt :: Ct -> Bool Source #

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

insolubleImplic :: Implication -> Bool Source #

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

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 :: TcLclEnv ic_wanted :: WantedConstraints ic_binds :: EvBindsVar ic_need_inner :: VarSet ic_need_outer :: VarSet ic_status :: ImplicStatus

Instances

Instances details

Outputable Implication Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: Implication -> SDoc Source #

implicationPrototype :: Implication Source #

checkTelescopeSkol :: SkolemInfoAnon -> Bool Source #

data ImplicStatus Source #

Constructors

IC_Solved
Fields ics_dead :: [EvVar]
IC_Insoluble
IC_BadTelescope
IC_Unsolved

Instances

Instances details

Outputable ImplicStatus Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: ImplicStatus -> SDoc Source #

isInsolubleStatus :: ImplicStatus -> Bool Source #

isSolvedStatus :: ImplicStatus -> Bool Source #

type UserGiven = Implication Source #

getUserGivensFromImplics :: [Implication] -> [UserGiven] Source #

data HasGivenEqs Source #

Constructors

NoGivenEqs
LocalGivenEqs
MaybeGivenEqs

Instances

Instances details

Monoid HasGivenEqs Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods mempty :: HasGivenEqs Source # mappend :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs Source # mconcat :: [HasGivenEqs] -> HasGivenEqs Source #
Semigroup HasGivenEqs Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods (<>) :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs Source # sconcat :: NonEmpty HasGivenEqs -> HasGivenEqs Source # stimes :: Integral b => b -> HasGivenEqs -> HasGivenEqs Source #
Outputable HasGivenEqs Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: HasGivenEqs -> SDoc Source #
Eq HasGivenEqs Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods (==) :: HasGivenEqs -> HasGivenEqs -> Bool # (/=) :: HasGivenEqs -> HasGivenEqs -> Bool #

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

data SubGoalDepth Source #

See Note [SubGoalDepth]

Instances

Instances details

Outputable SubGoalDepth Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: SubGoalDepth -> SDoc Source #
Eq SubGoalDepth Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods (==) :: SubGoalDepth -> SubGoalDepth -> Bool # (/=) :: SubGoalDepth -> SubGoalDepth -> Bool #
Ord SubGoalDepth Source #
Instance details 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 Source #

maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth Source #

bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth Source #

subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool Source #

data CtLoc Source #

Constructors

CtLoc
Fields ctl_origin :: CtOrigin ctl_env :: TcLclEnv ctl_t_or_k :: Maybe TypeOrKind ctl_depth :: !SubGoalDepth

ctLocSpan :: CtLoc -> RealSrcSpan Source #

ctLocEnv :: CtLoc -> TcLclEnv Source #

ctLocLevel :: CtLoc -> TcLevel Source #

ctLocOrigin :: CtLoc -> CtOrigin Source #

ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind Source #

ctLocDepth :: CtLoc -> SubGoalDepth Source #

bumpCtLocDepth :: CtLoc -> CtLoc Source #

isGivenLoc :: CtLoc -> Bool Source #

setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc Source #

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

setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc Source #

setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc Source #

pprCtLoc :: CtLoc -> SDoc Source #

data CtEvidence Source #

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

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 #

mkKindLoc :: TcType -> TcType -> CtLoc -> CtLoc Source #

toKindLoc :: CtLoc -> CtLoc Source #

Take a CtLoc and moves it to the kind level

mkGivenLoc :: TcLevel -> SkolemInfoAnon -> TcLclEnv -> CtLoc Source #

isWanted :: CtEvidence -> Bool Source #

isGiven :: CtEvidence -> Bool Source #

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

setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence Source #

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.

ctEvUnique :: CtEvidence -> Unique Source #

tcEvDestUnique :: TcEvDest -> Unique Source #

newtype RewriterSet Source #

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

Constructors

RewriterSet (UniqSet CoercionHole)

Instances

Instances details

Monoid RewriterSet Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods mempty :: RewriterSet Source # mappend :: RewriterSet -> RewriterSet -> RewriterSet Source # mconcat :: [RewriterSet] -> RewriterSet Source #
Semigroup RewriterSet Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods (<>) :: RewriterSet -> RewriterSet -> RewriterSet Source # sconcat :: NonEmpty RewriterSet -> RewriterSet Source # stimes :: Integral b => b -> RewriterSet -> RewriterSet Source #
Outputable RewriterSet Source #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: RewriterSet -> SDoc Source #

emptyRewriterSet :: RewriterSet Source #

isEmptyRewriterSet :: RewriterSet -> Bool Source #

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.

addRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet Source #

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

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 Methods (==) :: CtFlavour -> CtFlavour -> Bool # (/=) :: CtFlavour -> CtFlavour -> Bool #

ctEvFlavour :: CtEvidence -> CtFlavour Source #

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

eqCanRewrite :: EqRel -> EqRel -> Bool Source #

eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool Source #

pprEvVarTheta :: [EvVar] -> SDoc Source #

pprEvVars :: [EvVar] -> SDoc Source #

pprEvVarWithType :: EvVar -> SDoc Source #