Safe Haskell	Ignore
Language	GHC2021

GHC.Tc.Types.Constraint

Description

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

Synopsis

type Xi = TcType
data Ct
- = CDictCan DictCt
- | CIrredCan IrredCt
- | CEqCan EqCt
- | CQuantCan QCInst
- | CNonCanonical CtEvidence
type Cts = Bag Ct
singleCt :: Ct -> Cts
listToCts :: [Ct] -> Cts
ctsElts :: Cts -> [Ct]
consCts :: Ct -> Cts -> Cts
snocCts :: Cts -> Ct -> Cts
extendCtsList :: Cts -> [Ct] -> Cts
isEmptyCts :: Cts -> Bool
emptyCts :: Cts
andCts :: Cts -> Cts -> Cts
ctsPreds :: Cts -> [PredType]
isPendingScDictCt :: DictCt -> Bool
isPendingScDict :: Ct -> Bool
pendingScDict_maybe :: Ct -> Maybe Ct
superClassesMightHelp :: WantedConstraints -> Bool
getPendingWantedScs :: Cts -> ([Ct], Cts)
isWantedCt :: Ct -> Bool
isGivenCt :: Ct -> Bool
isTopLevelUserTypeError :: PredType -> Bool
containsUserTypeError :: PredType -> Bool
getUserTypeErrorMsg :: PredType -> Maybe ErrorMsgType
isUnsatisfiableCt_maybe :: Type -> Maybe ErrorMsgType
ctEvidence :: Ct -> CtEvidence
updCtEvidence :: (CtEvidence -> CtEvidence) -> Ct -> Ct
ctLoc :: Ct -> CtLoc
ctPred :: Ct -> PredType
ctFlavour :: Ct -> CtFlavour
ctEqRel :: Ct -> EqRel
ctOrigin :: Ct -> CtOrigin
ctRewriters :: Ct -> RewriterSet
ctHasNoRewriters :: Ct -> Bool
wantedCtHasNoRewriters :: WantedCtEvidence -> Bool
ctEvId :: HasDebugCallStack => Ct -> EvVar
wantedEvId_maybe :: Ct -> Maybe EvVar
mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
mkNonCanonical :: CtEvidence -> Ct
mkGivens :: CtLoc -> [EvId] -> [Ct]
tyCoVarsOfCt :: Ct -> TcTyCoVarSet
tyCoVarsOfCts :: Cts -> TcTyCoVarSet
tyCoVarsOfCtList :: Ct -> [TcTyCoVar]
tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]
boundOccNamesOfWC :: WantedConstraints -> [OccName]
data EqCt = EqCt {
- eq_ev :: CtEvidence
- eq_lhs :: CanEqLHS
- eq_rhs :: Xi
- eq_eq_rel :: EqRel
}
eqCtEvidence :: EqCt -> CtEvidence
eqCtLHS :: EqCt -> CanEqLHS
data DictCt = DictCt {
- di_ev :: CtEvidence
- di_cls :: Class
- di_tys :: [Xi]
- di_pend_sc :: ExpansionFuel
}
dictCtEvidence :: DictCt -> CtEvidence
dictCtPred :: DictCt -> TcPredType
data IrredCt = IrredCt {
- ir_ev :: CtEvidence
- ir_reason :: CtIrredReason
}
irredCtEvidence :: IrredCt -> CtEvidence
mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
ctIrredCt :: CtIrredReason -> Ct -> IrredCt
irredCtPred :: IrredCt -> PredType
data QCInst = QCI {
- qci_ev :: CtEvidence
- qci_tvs :: [TcTyVar]
- qci_theta :: TcThetaType
- qci_body :: TcPredType
- qci_pend_sc :: ExpansionFuel
}
pendingScInst_maybe :: QCInst -> Maybe QCInst
type ExpansionFuel = Int
doNotExpand :: ExpansionFuel
consumeFuel :: ExpansionFuel -> ExpansionFuel
pendingFuel :: ExpansionFuel -> Bool
assertFuelPrecondition :: ExpansionFuel -> a -> a
assertFuelPreconditionStrict :: ExpansionFuel -> a -> a
data CtIrredReason
- = IrredShapeReason
- | NonCanonicalReason CheckTyEqResult
- | ReprEqReason
- | ShapeMismatchReason
- | AbstractTyConReason
- | PluginReason
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
cteConcrete :: CheckTyEqProblem
cteSkolemEscape :: CheckTyEqProblem
impredicativeProblem :: CheckTyEqResult
insolubleOccursProblem :: CheckTyEqResult
solubleOccursProblem :: CheckTyEqResult
cterHasNoProblem :: CheckTyEqResult -> Bool
cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
cterHasOnlyProblems :: CheckTyEqResult -> CheckTyEqResult -> Bool
cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
cterHasOccursCheck :: CheckTyEqResult -> Bool
cterFromKind :: CheckTyEqResult -> CheckTyEqResult
data CanEqLHS
- = TyVarLHS TyVar
- | TyFamLHS TyCon [Type]
canEqLHS_maybe :: Type -> Maybe CanEqLHS
canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
canEqLHSKind :: CanEqLHS -> Kind
canEqLHSType :: CanEqLHS -> Type
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
- | DE_Multiplicity TcCoercion CtLoc
data NotConcreteError = NCE_FRR {
- nce_loc :: CtLoc
- nce_frr_origin :: FixedRuntimeRepOrigin
}
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 IrredCt -> WantedConstraints
dropMisleading :: WantedConstraints -> WantedConstraints
addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints
addNotConcreteError :: WantedConstraints -> NotConcreteError -> WantedConstraints
addMultiplicityCoercionError :: WantedConstraints -> TcCoercion -> CtLoc -> WantedConstraints
addDelayedErrors :: WantedConstraints -> Bag DelayedError -> WantedConstraints
tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]
insolubleWantedCt :: Ct -> Bool
insolubleCt :: Ct -> Bool
insolubleIrredCt :: IrredCt -> Bool
insolubleImplic :: Implication -> Bool
nonDefaultableTyVarsOfWC :: WantedConstraints -> TyCoVarSet
approximateWCX :: Bool -> WantedConstraints -> ApproxWC
approximateWC :: Bool -> WantedConstraints -> Bag Ct
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 :: !CtLocEnv
- ic_wanted :: WantedConstraints
- ic_binds :: EvBindsVar
- ic_need :: EvNeedSet
- ic_need_implic :: EvNeedSet
- ic_status :: ImplicStatus
}
implicationPrototype :: CtLocEnv -> 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 EvNeedSet = ENS {
- ens_dms :: VarSet
- ens_fvs :: VarSet
}
emptyEvNeedSet :: EvNeedSet
unionEvNeedSet :: EvNeedSet -> EvNeedSet -> EvNeedSet
extendEvNeedSet :: EvNeedSet -> Var -> EvNeedSet
delGivensFromEvNeedSet :: EvNeedSet -> [Var] -> EvNeedSet
data CtLocEnv = CtLocEnv {
- ctl_ctxt :: ![ErrCtxt]
- ctl_loc :: !RealSrcSpan
- ctl_bndrs :: !TcBinderStack
- ctl_tclvl :: !TcLevel
- ctl_in_gen_code :: !Bool
- ctl_rdr :: !LocalRdrEnv
}
setCtLocEnvLoc :: CtLocEnv -> SrcSpan -> CtLocEnv
setCtLocEnvLvl :: CtLocEnv -> TcLevel -> CtLocEnv
getCtLocEnvLoc :: CtLocEnv -> RealSrcSpan
getCtLocEnvLvl :: CtLocEnv -> TcLevel
ctLocEnvInGeneratedCode :: CtLocEnv -> Bool
data CtEvidence
- = CtGiven GivenCtEvidence
- | CtWanted WantedCtEvidence
data TcEvDest
- = EvVarDest EvVar
- | HoleDest CoercionHole
isWanted :: CtEvidence -> Bool
isGiven :: CtEvidence -> Bool
ctEvPred :: CtEvidence -> TcPredType
ctEvLoc :: CtEvidence -> CtLoc
ctEvOrigin :: CtEvidence -> CtOrigin
ctEvEqRel :: HasDebugCallStack => CtEvidence -> EqRel
ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr
ctEvTerm :: CtEvidence -> EvTerm
ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion
givenCtEvCoercion :: GivenCtEvidence -> TcCoercion
ctEvEvId :: CtEvidence -> EvVar
wantedCtEvEvId :: WantedCtEvidence -> EvVar
ctEvRewriters :: CtEvidence -> RewriterSet
setWantedCtEvRewriters :: WantedCtEvidence -> RewriterSet -> WantedCtEvidence
ctEvUnique :: CtEvidence -> Unique
tcEvDestUnique :: TcEvDest -> Unique
ctEvRewriteRole :: HasDebugCallStack => CtEvidence -> Role
ctEvRewriteEqRel :: CtEvidence -> EqRel
setCtEvPredType :: HasDebugCallStack => CtEvidence -> Type -> CtEvidence
setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence
tyCoVarsOfCtEvList :: CtEvidence -> [TcTyCoVar]
tyCoVarsOfCtEv :: CtEvidence -> TcTyCoVarSet
tyCoVarsOfCtEvsList :: [CtEvidence] -> [TcTyCoVar]
data GivenCtEvidence = GivenCt {
- ctev_pred :: TcPredType
- ctev_evar :: EvVar
- ctev_loc :: CtLoc
}
data WantedCtEvidence = WantedCt {
- ctev_pred :: TcPredType
- ctev_dest :: TcEvDest
- ctev_loc :: CtLoc
- ctev_rewriters :: RewriterSet
}
newtype RewriterSet = RewriterSet (UniqSet CoercionHole)
emptyRewriterSet :: RewriterSet
isEmptyRewriterSet :: RewriterSet -> Bool
addRewriter :: RewriterSet -> CoercionHole -> RewriterSet
unitRewriterSet :: CoercionHole -> RewriterSet
unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet
rewriterSetFromCts :: Bag Ct -> RewriterSet
wrapType :: Type -> [TyVar] -> [PredType] -> Type
data CtFlavour
- = Given
- | Wanted
ctEvFlavour :: CtEvidence -> CtFlavour
type CtFlavourRole = (CtFlavour, EqRel)
ctEvFlavourRole :: HasDebugCallStack => CtEvidence -> CtFlavourRole
ctFlavourRole :: HasDebugCallStack => Ct -> CtFlavourRole
eqCtFlavourRole :: EqCt -> CtFlavourRole
eqCanRewrite :: EqRel -> EqRel -> Bool
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
pprEvVarTheta :: [EvVar] -> SDoc
pprEvVars :: [EvVar] -> SDoc
pprEvVarWithType :: EvVar -> SDoc

Documentation

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 #

Constraint

Constructors

CDictCan DictCt	A dictionary constraint (canonical)
CIrredCan IrredCt	An irreducible constraint (non-canonical)
CEqCan EqCt	An equality constraint (canonical)
CQuantCan QCInst	A quantified constraint (canonical)
CNonCanonical CtEvidence	A non-canonical constraint See Note [NonCanonical Semantics] in GHC.Tc.Solver.Monad

Instances

Instances details

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

type Cts = Bag Ct #

singleCt :: Ct -> Cts #

listToCts :: [Ct] -> Cts #

ctsElts :: Cts -> [Ct] #

consCts :: Ct -> Cts -> Cts #

snocCts :: Cts -> Ct -> Cts #

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

isEmptyCts :: Cts -> Bool #

emptyCts :: Cts #

andCts :: Cts -> Cts -> Cts #

ctsPreds :: Cts -> [PredType] #

isPendingScDictCt :: DictCt -> Bool #

isPendingScDict :: Ct -> Bool #

pendingScDict_maybe :: 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 #

isGivenCt :: Ct -> Bool #

isTopLevelUserTypeError :: PredType -> Bool #

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

containsUserTypeError :: PredType -> Bool #

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 #

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 #

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

ctEvidence :: Ct -> CtEvidence #

updCtEvidence :: (CtEvidence -> CtEvidence) -> Ct -> Ct #

ctLoc :: Ct -> CtLoc #

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 #

ctRewriters :: Ct -> RewriterSet #

ctHasNoRewriters :: Ct -> Bool #

wantedCtHasNoRewriters :: WantedCtEvidence -> Bool #

ctEvId :: HasDebugCallStack => Ct -> EvVar #

wantedEvId_maybe :: Ct -> Maybe EvVar #

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

Returns Nothing otherwise.

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

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

mkNonCanonical :: CtEvidence -> Ct #

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

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.

boundOccNamesOfWC :: WantedConstraints -> [OccName] #

data EqCt #

A canonical equality constraint.

See Note [Canonical equalities] in GHC.Tc.Types.Constraint.

Constructors

EqCt
Fields eq_ev :: CtEvidence eq_lhs :: CanEqLHS eq_rhs :: Xi eq_eq_rel :: EqRel

Instances

Instances details

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

eqCtEvidence :: EqCt -> CtEvidence #

eqCtLHS :: EqCt -> CanEqLHS #

data DictCt #

A canonical dictionary constraint

Constructors

DictCt
Fields di_ev :: CtEvidence di_cls :: Class di_tys :: [Xi] di_pend_sc :: ExpansionFuel

Instances

Instances details

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

dictCtEvidence :: DictCt -> CtEvidence #

dictCtPred :: DictCt -> TcPredType #

data IrredCt #

Constructors

IrredCt
Fields ir_ev :: CtEvidence ir_reason :: CtIrredReason

Instances

Instances details

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

irredCtEvidence :: IrredCt -> CtEvidence #

mkIrredCt :: CtIrredReason -> CtEvidence -> Ct #

ctIrredCt :: CtIrredReason -> Ct -> IrredCt #

irredCtPred :: IrredCt -> PredType #

data QCInst #

A quantified constraint, also called a "local instance" (a simplified version of ClsInst).

See Note [Quantified constraints] in GHC.Tc.Solver.Solve

Constructors

QCI

A quantified constraint, of type forall tvs. context => ty

Fields

qci_ev :: CtEvidence
qci_tvs :: [TcTyVar]
```
tvs
```
qci_theta :: TcThetaType
qci_body :: TcPredType
the body of the forall, i.e. ty
qci_pend_sc :: ExpansionFuel
Invariants: qci_pend_sc > 0 =>
(a) qci_body is a ClassPred (b) this class has superclass(es), and (c) the superclass(es) are not explored yet
Same as di_pend_sc flag in DictCt See Note [Expanding Recursive Superclasses and ExpansionFuel] in GHC.Tc.Solver

Instances

Instances details

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

pendingScInst_maybe :: QCInst -> Maybe QCInst #

type ExpansionFuel = Int #

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

doNotExpand :: ExpansionFuel #

Do not expand superclasses any further

consumeFuel :: ExpansionFuel -> ExpansionFuel #

Consumes one unit of fuel. Precondition: fuel > 0

pendingFuel :: ExpansionFuel -> Bool #

Returns True if we have any fuel left for superclass expansion

assertFuelPrecondition :: ExpansionFuel -> a -> a #

asserts if fuel is non-negative

assertFuelPreconditionStrict :: ExpansionFuel -> a -> a #

asserts if fuel is strictly greater than 0

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`)
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 #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: CtIrredReason -> SDoc #

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

Instances details

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

data CheckTyEqProblem #

An individual problem that might be logged in a CheckTyEqResult

Instances

Instances details

Outputable CheckTyEqProblem #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: CheckTyEqProblem -> SDoc #
Eq CheckTyEqProblem #
Instance details Defined in GHC.Tc.Types.Constraint Methods (==) :: CheckTyEqProblem -> CheckTyEqProblem -> Bool # (/=) :: CheckTyEqProblem -> CheckTyEqProblem -> Bool #

cteProblem :: CheckTyEqProblem -> CheckTyEqResult #

cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult #

cteOK :: CheckTyEqResult #

No problems in checking the validity of a type equality.

cteImpredicative :: CheckTyEqProblem #

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

cteConcrete :: CheckTyEqProblem #

cteSkolemEscape :: CheckTyEqProblem #

impredicativeProblem :: CheckTyEqResult #

insolubleOccursProblem :: CheckTyEqResult #

solubleOccursProblem :: CheckTyEqResult #

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

cterHasOnlyProblems :: CheckTyEqResult -> CheckTyEqResult -> Bool #

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 TyVar
TyFamLHS
Fields TyCon TyCon of the family [Type] Arguments, exactly saturating the family

Instances

Instances details

Outputable CanEqLHS #
Instance details Defined in GHC.Core.Predicate Methods ppr :: CanEqLHS -> SDoc #

canEqLHS_maybe :: Type -> 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.

canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS #

canEqLHSKind :: CanEqLHS -> Kind #

Retrieve the kind of a CanEqLHS

canEqLHSType :: CanEqLHS -> Type #

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 in expressions] for holes in terms.

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 #
Instance details 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

Instances details

Outputable HoleSort #
Instance details 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 DelayedError #

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

DE_NotConcrete NotConcreteError

A type could not be ensured to be concrete.

See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.

DE_Multiplicity TcCoercion CtLoc

An error if the TcCoercion isn't a reflexivity constraint.

See Note [Coercion errors in tcSubMult] in GHC.Tc.Utils.Unify.

Instances

Instances details

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

data NotConcreteError #

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?

Instances

Instances details

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

data WantedConstraints #

Constructors

WC
Fields wc_simple :: Cts wc_impl :: Bag Implication wc_errors :: Bag DelayedError

Instances

Instances details

Outputable WantedConstraints #
Instance details 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 IrredCt -> WantedConstraints #

dropMisleading :: WantedConstraints -> WantedConstraints #

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

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

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

addNotConcreteError :: WantedConstraints -> NotConcreteError -> WantedConstraints #

addMultiplicityCoercionError :: WantedConstraints -> TcCoercion -> CtLoc -> WantedConstraints #

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

tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet #

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

tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar] #

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

insolubleWantedCt :: Ct -> Bool #

insolubleCt :: Ct -> Bool #

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

insolubleIrredCt :: IrredCt -> Bool #

insolubleImplic :: Implication -> Bool #

nonDefaultableTyVarsOfWC :: WantedConstraints -> TyCoVarSet #

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.

approximateWCX :: Bool -> WantedConstraints -> ApproxWC #

approximateWC :: Bool -> WantedConstraints -> Bag Ct #

data Implication #

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 :: !CtLocEnv ic_wanted :: WantedConstraints ic_binds :: EvBindsVar ic_need :: EvNeedSet ic_need_implic :: EvNeedSet ic_status :: ImplicStatus

Instances

Instances details

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

implicationPrototype :: CtLocEnv -> Implication #

checkTelescopeSkol :: SkolemInfoAnon -> Bool #

data ImplicStatus #

Constructors

IC_Solved
Fields ics_dead :: [EvVar]
IC_Insoluble
IC_BadTelescope
IC_Unsolved

Instances

Instances details

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

isInsolubleStatus :: ImplicStatus -> Bool #

isSolvedStatus :: ImplicStatus -> Bool #

type UserGiven = Implication #

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

data HasGivenEqs #

Constructors

NoGivenEqs
LocalGivenEqs
MaybeGivenEqs

Instances

Instances details

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

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

data EvNeedSet #

Constructors

ENS
Fields ens_dms :: VarSet ens_fvs :: VarSet

Instances

Instances details

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

emptyEvNeedSet :: EvNeedSet #

unionEvNeedSet :: EvNeedSet -> EvNeedSet -> EvNeedSet #

extendEvNeedSet :: EvNeedSet -> Var -> EvNeedSet #

delGivensFromEvNeedSet :: EvNeedSet -> [Var] -> EvNeedSet #

data CtLocEnv #

Local typechecker environment for a constraint.

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

Instances

Instances details

Outputable CtEvidence #
Instance details 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 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 #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: TcEvDest -> SDoc #

isWanted :: CtEvidence -> Bool #

isGiven :: CtEvidence -> Bool #

ctEvPred :: CtEvidence -> TcPredType #

ctEvLoc :: CtEvidence -> CtLoc #

ctEvOrigin :: CtEvidence -> CtOrigin #

ctEvEqRel :: HasDebugCallStack => CtEvidence -> EqRel #

Get the equality relation relevant for a CtEvidence

ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr #

ctEvTerm :: CtEvidence -> EvTerm #

ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion #

givenCtEvCoercion :: GivenCtEvidence -> TcCoercion #

ctEvEvId :: CtEvidence -> EvVar #

wantedCtEvEvId :: WantedCtEvidence -> EvVar #

ctEvRewriters :: CtEvidence -> RewriterSet #

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.

setWantedCtEvRewriters :: WantedCtEvidence -> RewriterSet -> WantedCtEvidence #

Set the rewriter set of a Wanted constraint.

ctEvUnique :: CtEvidence -> Unique #

tcEvDestUnique :: TcEvDest -> Unique #

ctEvRewriteRole :: HasDebugCallStack => CtEvidence -> Role #

Get the rewrite-role relevant for a CtEvidence See Note [The rewrite-role of a constraint]

ctEvRewriteEqRel :: CtEvidence -> EqRel #

Return the rewrite-role of an abitrary CtEvidence See Note [The rewrite-role of a constraint] We return ReprEq for (a ~R# b) and NomEq for all other preds

setCtEvPredType :: HasDebugCallStack => CtEvidence -> Type -> 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].

setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence #

tyCoVarsOfCtEvList :: CtEvidence -> [TcTyCoVar] #

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

tyCoVarsOfCtEv :: CtEvidence -> TcTyCoVarSet #

Returns free variables of constraints as a non-deterministic set

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

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

data GivenCtEvidence #

Evidence for a Given constraint

Constructors

GivenCt
Fields ctev_pred :: TcPredType ctev_evar :: EvVar ctev_loc :: CtLoc

Instances

Instances details

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

data WantedCtEvidence #

Evidence for a Wanted constraint

Constructors

WantedCt
Fields ctev_pred :: TcPredType ctev_dest :: TcEvDest ctev_loc :: CtLoc ctev_rewriters :: RewriterSet

Instances

Instances details

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

newtype RewriterSet #

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

emptyRewriterSet :: RewriterSet #

isEmptyRewriterSet :: RewriterSet -> Bool #

addRewriter :: RewriterSet -> CoercionHole -> RewriterSet #

unitRewriterSet :: CoercionHole -> RewriterSet #

unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet #

rewriterSetFromCts :: Bag Ct -> RewriterSet #

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

data CtFlavour #

Constructors

Given
Wanted

Instances

Instances details

Outputable CtFlavour #
Instance details Defined in GHC.Tc.Types.Constraint Methods ppr :: CtFlavour -> SDoc #
Eq CtFlavour #
Instance details Defined in GHC.Tc.Types.Constraint Methods (==) :: CtFlavour -> CtFlavour -> Bool # (/=) :: CtFlavour -> CtFlavour -> Bool #

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

ctEvFlavourRole :: HasDebugCallStack => CtEvidence -> CtFlavourRole #

Extract the flavour, role, and boxity from a CtEvidence

ctFlavourRole :: HasDebugCallStack => Ct -> CtFlavourRole #

Extract the flavour and role from a Ct

eqCtFlavourRole :: EqCt -> CtFlavourRole #

Extract the flavour and role from a Ct

eqCanRewrite :: EqRel -> EqRel -> Bool #

eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool #

pprEvVarTheta :: [EvVar] -> SDoc #

pprEvVars :: [EvVar] -> SDoc #

pprEvVarWithType :: EvVar -> SDoc #

CtLocEnv
Fields ctl_ctxt :: ![ErrCtxt] ctl_loc :: !RealSrcSpan ctl_bndrs :: !TcBinderStack ctl_tclvl :: !TcLevel ctl_in_gen_code :: !Bool ctl_rdr :: !LocalRdrEnv