Safe Haskell | None |
---|---|
Language | GHC2021 |
This module defines types and simple operations over constraints, as used in the type-checker and constraint solver.
Synopsis
- type Xi = TcType
- data Ct
- 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
- 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 {}
- 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 {}
- irredCtEvidence :: IrredCt -> CtEvidence
- mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
- ctIrredCt :: CtIrredReason -> Ct -> IrredCt
- irredCtPred :: IrredCt -> PredType
- data QCInst = QCI {
- qci_ev :: CtEvidence
- qci_tvs :: [TcTyVar]
- qci_pred :: 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
- isInsolubleReason :: CtIrredReason -> Bool
- data CheckTyEqResult
- data CheckTyEqProblem
- cteProblem :: CheckTyEqProblem -> CheckTyEqResult
- cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult
- cteOK :: CheckTyEqResult
- cteImpredicative :: CheckTyEqProblem
- cteTypeFamily :: CheckTyEqProblem
- cteCoercionHole :: 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
- canEqLHS_maybe :: Xi -> Maybe CanEqLHS
- canTyFamEqLHS_maybe :: Xi -> Maybe CanEqLHS
- canEqLHSKind :: CanEqLHS -> TcKind
- canEqLHSType :: CanEqLHS -> TcType
- eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
- data Hole = Hole {}
- data HoleSort
- isOutOfScopeHole :: Hole -> Bool
- data DelayedError
- data NotConcreteError = NCE_FRR {}
- data NotConcreteReason
- data WantedConstraints = WC {}
- 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 :: WantedConstraints -> ApproxWC
- approximateWC :: Bool -> WantedConstraints -> Bag Ct
- data Implication = Implic {}
- implicationPrototype :: CtLocEnv -> Implication
- checkTelescopeSkol :: SkolemInfoAnon -> Bool
- data ImplicStatus
- = IC_Solved { }
- | IC_Insoluble
- | IC_BadTelescope
- | IC_Unsolved
- isInsolubleStatus :: ImplicStatus -> Bool
- isSolvedStatus :: ImplicStatus -> Bool
- type UserGiven = Implication
- getUserGivensFromImplics :: [Implication] -> [UserGiven]
- data HasGivenEqs
- checkImplicationInvariants :: (HasCallStack, Applicative m) => Implication -> m ()
- 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
- data TcEvDest
- 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
- ctEvEvId :: CtEvidence -> EvVar
- ctEvRewriters :: CtEvidence -> RewriterSet
- 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]
- 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
- 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
Instances
isEmptyCts :: Cts -> Bool Source #
isPendingScDictCt :: DictCt -> Bool Source #
isPendingScDict :: Ct -> Bool 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]
isWantedCt :: Ct -> Bool Source #
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.
ctEvidence :: Ct -> CtEvidence Source #
updCtEvidence :: (CtEvidence -> CtEvidence) -> Ct -> Ct Source #
ctRewriters :: Ct -> RewriterSet Source #
mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType Source #
Makes a new equality predicate with the same role as the given evidence.
mkNonCanonical :: CtEvidence -> 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.
boundOccNamesOfWC :: WantedConstraints -> [OccName] Source #
Instances
eqCtEvidence :: EqCt -> CtEvidence Source #
DictCt | |
|
Instances
dictCtEvidence :: DictCt -> CtEvidence Source #
dictCtPred :: DictCt -> TcPredType Source #
Instances
irredCtEvidence :: IrredCt -> CtEvidence Source #
mkIrredCt :: CtIrredReason -> CtEvidence -> Ct Source #
irredCtPred :: IrredCt -> PredType Source #
QCI | |
|
Instances
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
IrredShapeReason | This constraint has a non-canonical shape (e.g. |
NonCanonicalReason CheckTyEqResult | An equality where some invariant other than (TyEq:H) of |
ReprEqReason | An equality that cannot be decomposed because it is representational.
Example: |
ShapeMismatchReason | A nominal equality that relates two wholly different types,
like |
AbstractTyConReason | An equality like |
PluginReason | A typechecker plugin returned this in the pluginBadCts field of TcPluginProgress |
Instances
Outputable CtIrredReason Source # | |
Defined in GHC.Tc.Types.Constraint 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
Outputable CheckTyEqResult Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: CheckTyEqResult -> SDoc Source # | |
Monoid CheckTyEqResult Source # | |
Defined in GHC.Tc.Types.Constraint mappend :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult # mconcat :: [CheckTyEqResult] -> CheckTyEqResult # | |
Semigroup CheckTyEqResult Source # | |
Defined in GHC.Tc.Types.Constraint (<>) :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult # sconcat :: NonEmpty CheckTyEqResult -> CheckTyEqResult # stimes :: Integral b => b -> CheckTyEqResult -> CheckTyEqResult # |
data CheckTyEqProblem Source #
An individual problem that might be logged in a CheckTyEqResult
Instances
Outputable CheckTyEqProblem Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: CheckTyEqProblem -> SDoc Source # | |
Eq CheckTyEqProblem Source # | |
Defined in GHC.Tc.Types.Constraint (==) :: CheckTyEqProblem -> CheckTyEqProblem -> Bool # (/=) :: CheckTyEqProblem -> CheckTyEqProblem -> Bool # |
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.
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
cterFromKind :: CheckTyEqResult -> CheckTyEqResult Source #
Retain only information about occurs-check failures, because only that matters after recurring into a kind.
A CanEqLHS
is a type that can appear on the left of a canonical
equality: a type variable or exactly-saturated type family application.
Instances
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.
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].
Instances
Used to indicate which sort of hole we have.
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
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.
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. |
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
Outputable DelayedError Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: DelayedError -> SDoc Source # |
data NotConcreteError Source #
Why did we require that a certain type be concrete?
NCE_FRR | Concreteness was required by a representation-polymorphism check. See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. |
|
Instances
Outputable NotConcreteError Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: NotConcreteError -> SDoc Source # |
data NotConcreteReason Source #
Why did we decide that a type was not concrete?
NonConcreteTyCon TyCon [TcType] | The type contains a 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 |
data WantedConstraints Source #
WC | |
|
Instances
Outputable WantedConstraints Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: WantedConstraints -> SDoc Source # |
insolubleWC :: WantedConstraints -> Bool 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.
mkSimpleWC :: [CtEvidence] -> WantedConstraints Source #
addInsols :: WantedConstraints -> Bag IrredCt -> WantedConstraints Source #
addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints Source #
addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints Source #
addMultiplicityCoercionError :: WantedConstraints -> TcCoercion -> CtLoc -> 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 #
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
insolubleIrredCt :: IrredCt -> Bool Source #
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.
approximateWCX :: WantedConstraints -> ApproxWC Source #
approximateWC :: Bool -> WantedConstraints -> Bag Ct Source #
data Implication Source #
Implic | |
|
Instances
Outputable Implication Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: Implication -> SDoc Source # |
data ImplicStatus Source #
Instances
Outputable ImplicStatus Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: ImplicStatus -> SDoc Source # |
isInsolubleStatus :: ImplicStatus -> Bool Source #
isSolvedStatus :: ImplicStatus -> Bool Source #
type UserGiven = Implication Source #
getUserGivensFromImplics :: [Implication] -> [UserGiven] Source #
data HasGivenEqs Source #
Instances
Outputable HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: HasGivenEqs -> SDoc Source # | |
Monoid HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint mempty :: HasGivenEqs # mappend :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs # mconcat :: [HasGivenEqs] -> HasGivenEqs # | |
Semigroup HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint (<>) :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs # sconcat :: NonEmpty HasGivenEqs -> HasGivenEqs # stimes :: Integral b => b -> HasGivenEqs -> HasGivenEqs # | |
Eq HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint (==) :: HasGivenEqs -> HasGivenEqs -> Bool # (/=) :: HasGivenEqs -> HasGivenEqs -> Bool # |
checkImplicationInvariants :: (HasCallStack, Applicative m) => Implication -> m () Source #
Local typechecker environment for a constraint.
Used to restore the environment of a constraint
when reporting errors, see setCtLocM
.
See also TcLclCtxt
.
CtLocEnv | |
|
getCtLocEnvLoc :: CtLocEnv -> RealSrcSpan Source #
getCtLocEnvLvl :: CtLocEnv -> TcLevel Source #
data CtEvidence Source #
CtGiven | |
CtWanted | |
|
Instances
Outputable CtEvidence Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: CtEvidence -> SDoc Source # |
A place for type-checking evidence to go after it is generated.
- Wanted equalities use HoleDest,
- other Wanteds use EvVarDest.
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
isWanted :: CtEvidence -> Bool Source #
isGiven :: CtEvidence -> Bool Source #
ctEvPred :: CtEvidence -> TcPredType Source #
ctEvLoc :: CtEvidence -> CtLoc Source #
ctEvOrigin :: CtEvidence -> CtOrigin Source #
ctEvEqRel :: HasDebugCallStack => 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.
ctEvUnique :: CtEvidence -> Unique Source #
tcEvDestUnique :: TcEvDest -> Unique Source #
ctEvRewriteRole :: HasDebugCallStack => CtEvidence -> Role Source #
Get the rewrite-role relevant for a CtEvidence
See Note [The rewrite-role of a constraint]
ctEvRewriteEqRel :: CtEvidence -> EqRel Source #
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 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.
newtype RewriterSet Source #
Stores a set of CoercionHoles that have been used to rewrite a constraint. See Note [Wanteds rewrite Wanteds].
Instances
Outputable RewriterSet Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: RewriterSet -> SDoc Source # | |
Monoid RewriterSet Source # | |
Defined in GHC.Tc.Types.Constraint mempty :: RewriterSet # mappend :: RewriterSet -> RewriterSet -> RewriterSet # mconcat :: [RewriterSet] -> RewriterSet # | |
Semigroup RewriterSet Source # | |
Defined in GHC.Tc.Types.Constraint (<>) :: RewriterSet -> RewriterSet -> RewriterSet # sconcat :: NonEmpty RewriterSet -> RewriterSet # stimes :: Integral b => b -> RewriterSet -> RewriterSet # |
isEmptyRewriterSet :: RewriterSet -> Bool Source #
addRewriter :: RewriterSet -> CoercionHole -> RewriterSet Source #
unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet Source #
rewriterSetFromCts :: Bag Ct -> RewriterSet Source #
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 :: HasDebugCallStack => CtEvidence -> CtFlavourRole Source #
Extract the flavour, role, and boxity from a CtEvidence
ctFlavourRole :: HasDebugCallStack => Ct -> CtFlavourRole Source #
Extract the flavour and role from a Ct
eqCtFlavourRole :: EqCt -> CtFlavourRole Source #
Extract the flavour and role from a Ct
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool Source #
pprEvVarTheta :: [EvVar] -> SDoc Source #
pprEvVarWithType :: EvVar -> SDoc Source #