Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
- isPendingScInst :: QCInst -> Maybe QCInst
- type Xi = TcType
- data Ct
- = CDictCan {
- cc_ev :: CtEvidence
- cc_class :: Class
- cc_tyargs :: [Xi]
- cc_pend_sc :: Bool
- | CIrredCan { }
- | CEqCan { }
- | CNonCanonical {
- cc_ev :: CtEvidence
- | CQuantCan QCInst
- = CDictCan {
- type Cts = Bag Ct
- emptyCts :: Cts
- andCts :: Cts -> Cts -> Cts
- andManyCts :: [Cts] -> Cts
- pprCts :: Cts -> SDoc
- singleCt :: Ct -> Cts
- listToCts :: [Ct] -> Cts
- ctsElts :: Cts -> [Ct]
- consCts :: Ct -> Cts -> Cts
- snocCts :: Cts -> Ct -> Cts
- extendCtsList :: Cts -> [Ct] -> Cts
- isEmptyCts :: Cts -> Bool
- isPendingScDict :: Ct -> Maybe Ct
- superClassesMightHelp :: WantedConstraints -> Bool
- getPendingWantedScs :: Cts -> ([Ct], Cts)
- isWantedCt :: Ct -> Bool
- isDerivedCt :: Ct -> Bool
- isGivenCt :: Ct -> Bool
- isUserTypeErrorCt :: Ct -> Bool
- getUserTypeErrorMsg :: Ct -> Maybe Type
- ctEvidence :: Ct -> CtEvidence
- ctLoc :: Ct -> CtLoc
- setCtLoc :: Ct -> CtLoc -> Ct
- ctPred :: Ct -> PredType
- ctFlavour :: Ct -> CtFlavour
- ctEqRel :: Ct -> EqRel
- ctOrigin :: Ct -> CtOrigin
- ctEvId :: Ct -> 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 :: CtEvidence -> EvExpr
- ctEvTerm :: CtEvidence -> EvTerm
- ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion
- ctEvEvId :: CtEvidence -> EvVar
- tyCoVarsOfCt :: Ct -> TcTyCoVarSet
- tyCoVarsOfCts :: Cts -> TcTyCoVarSet
- tyCoVarsOfCtList :: Ct -> [TcTyCoVar]
- tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]
- data CtIrredReason
- type HoleSet = UniqSet CoercionHole
- isInsolubleReason :: CtIrredReason -> Bool
- data CheckTyEqResult
- data CheckTyEqProblem
- cteProblem :: CheckTyEqProblem -> CheckTyEqResult
- cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult
- cteOK :: CheckTyEqResult
- cteImpredicative :: CheckTyEqProblem
- cteTypeFamily :: CheckTyEqProblem
- cteHoleBlocker :: 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
- canEqLHS_maybe :: Xi -> Maybe CanEqLHS
- canEqLHSKind :: CanEqLHS -> TcKind
- canEqLHSType :: CanEqLHS -> TcType
- eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
- data Hole = Hole {}
- data HoleSort
- isOutOfScopeHole :: Hole -> Bool
- 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 Ct -> WantedConstraints
- dropMisleading :: WantedConstraints -> WantedConstraints
- addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
- addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
- addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints
- tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
- dropDerivedWC :: WantedConstraints -> WantedConstraints
- dropDerivedSimples :: Cts -> Cts
- tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]
- insolubleCt :: Ct -> Bool
- insolubleEqCt :: Ct -> Bool
- isDroppableCt :: Ct -> Bool
- insolubleImplic :: Implication -> Bool
- arisesFromGivens :: Ct -> Bool
- data Implication = Implic {}
- implicationPrototype :: Implication
- checkTelescopeSkol :: SkolemInfo -> Bool
- data ImplicStatus
- = IC_Solved { }
- | IC_Insoluble
- | IC_BadTelescope
- | IC_Unsolved
- isInsolubleStatus :: ImplicStatus -> Bool
- isSolvedStatus :: ImplicStatus -> Bool
- data HasGivenEqs
- data SubGoalDepth
- initialSubGoalDepth :: SubGoalDepth
- maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
- bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
- subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
- data CtLoc = CtLoc {}
- 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
- data TcEvDest
- mkKindLoc :: TcType -> TcType -> CtLoc -> CtLoc
- toKindLoc :: CtLoc -> CtLoc
- mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
- isWanted :: CtEvidence -> Bool
- isGiven :: CtEvidence -> Bool
- isDerived :: CtEvidence -> Bool
- ctEvRole :: CtEvidence -> Role
- wrapType :: Type -> [TyVar] -> [PredType] -> Type
- data CtFlavour
- = Given
- | Wanted ShadowInfo
- | Derived
- data ShadowInfo
- ctFlavourContainsDerived :: CtFlavour -> Bool
- ctEvFlavour :: CtEvidence -> CtFlavour
- type CtFlavourRole = (CtFlavour, EqRel)
- ctEvFlavourRole :: CtEvidence -> CtFlavourRole
- ctFlavourRole :: Ct -> CtFlavourRole
- eqCanRewrite :: EqRel -> EqRel -> Bool
- eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
- eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
- eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
- pprEvVarTheta :: [EvVar] -> SDoc
- pprEvVars :: [EvVar] -> SDoc
- pprEvVarWithType :: EvVar -> SDoc
Documentation
QCI | |
|
Instances
CDictCan | |
| |
CIrredCan | |
CEqCan | |
CNonCanonical | |
| |
CQuantCan QCInst |
Instances
andManyCts :: [Cts] -> Cts Source #
isEmptyCts :: Cts -> 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 #
isDerivedCt :: Ct -> Bool Source #
isUserTypeErrorCt :: Ct -> Bool Source #
getUserTypeErrorMsg :: Ct -> 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 #
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 #
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 :: CtEvidence -> EvExpr Source #
ctEvTerm :: CtEvidence -> EvTerm Source #
ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion Source #
ctEvEvId :: CtEvidence -> EvVar Source #
tyCoVarsOfCt :: Ct -> TcTyCoVarSet Source #
Returns free variables of constraints as a non-deterministic set
tyCoVarsOfCts :: Cts -> TcTyCoVarSet Source #
Returns free variables of a bag of constraints as a non-deterministic set. See Note [Deterministic FV] in GHC.Utils.FV.
tyCoVarsOfCtList :: Ct -> [TcTyCoVar] Source #
Returns free variables of constraints as a deterministically ordered. list. See Note [Deterministic FV] in GHC.Utils.FV.
tyCoVarsOfCtsList :: Cts -> [TcTyCoVar] Source #
Returns free variables of a bag of constraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.
data CtIrredReason Source #
Used to indicate extra information about why a CIrredCan is irreducible
IrredShapeReason | this constraint has a non-canonical shape (e.g. |
HoleBlockerReason HoleSet | this constraint is blocked on the coercion hole(s) listed See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical Wrinkle (4a). Why store the HoleSet? See Wrinkle (2) of that same Note. INVARIANT: A HoleBlockerReason constraint is a homogeneous equality whose left hand side can fit in a CanEqLHS. |
NonCanonicalReason CheckTyEqResult | an equality where some invariant other than (TyEq:H) of |
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 |
Instances
Outputable CtIrredReason Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: CtIrredReason -> SDoc Source # |
type HoleSet = UniqSet CoercionHole Source #
A set of CoercionHole
s
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
Monoid CheckTyEqResult Source # | |
Defined in GHC.Tc.Types.Constraint | |
Semigroup CheckTyEqResult Source # | |
Defined in GHC.Tc.Types.Constraint (<>) :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult Source # sconcat :: NonEmpty CheckTyEqResult -> CheckTyEqResult Source # stimes :: Integral b => b -> CheckTyEqResult -> CheckTyEqResult Source # | |
Outputable CheckTyEqResult Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: CheckTyEqResult -> SDoc Source # |
data CheckTyEqProblem Source #
An individual problem that might be logged in a CheckTyEqResult
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 WantedConstraints Source #
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 Ct -> WantedConstraints Source #
addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints Source #
addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints Source #
tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet Source #
Returns free variables of WantedConstraints as a non-deterministic set. See Note [Deterministic FV] in GHC.Utils.FV.
dropDerivedSimples :: Cts -> Cts Source #
tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar] Source #
Returns free variables of WantedConstraints as a deterministically ordered list. See Note [Deterministic FV] in GHC.Utils.FV.
insolubleCt :: Ct -> Bool Source #
insolubleEqCt :: Ct -> Bool Source #
isDroppableCt :: Ct -> Bool Source #
insolubleImplic :: Implication -> Bool Source #
arisesFromGivens :: Ct -> Bool Source #
data Implication Source #
Implic | |
|
Instances
Outputable Implication Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: Implication -> SDoc Source # |
checkTelescopeSkol :: SkolemInfo -> Bool 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 #
data HasGivenEqs Source #
Instances
Monoid HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint mempty :: HasGivenEqs Source # mappend :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs Source # mconcat :: [HasGivenEqs] -> HasGivenEqs Source # | |
Semigroup HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint (<>) :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs Source # sconcat :: NonEmpty HasGivenEqs -> HasGivenEqs Source # stimes :: Integral b => b -> HasGivenEqs -> HasGivenEqs Source # | |
Outputable HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: HasGivenEqs -> SDoc Source # | |
Eq HasGivenEqs Source # | |
Defined in GHC.Tc.Types.Constraint (==) :: HasGivenEqs -> HasGivenEqs -> Bool # (/=) :: HasGivenEqs -> HasGivenEqs -> Bool # |
data SubGoalDepth Source #
See Note [SubGoalDepth]
Instances
Outputable SubGoalDepth Source # | |
Defined in GHC.Tc.Types.Constraint ppr :: SubGoalDepth -> SDoc Source # | |
Eq SubGoalDepth Source # | |
Defined in GHC.Tc.Types.Constraint (==) :: SubGoalDepth -> SubGoalDepth -> Bool # (/=) :: SubGoalDepth -> SubGoalDepth -> Bool # | |
Ord SubGoalDepth Source # | |
Defined in GHC.Tc.Types.Constraint compare :: SubGoalDepth -> SubGoalDepth -> Ordering # (<) :: SubGoalDepth -> SubGoalDepth -> Bool # (<=) :: SubGoalDepth -> SubGoalDepth -> Bool # (>) :: SubGoalDepth -> SubGoalDepth -> Bool # (>=) :: SubGoalDepth -> SubGoalDepth -> Bool # max :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth # min :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth # |
subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool Source #
CtLoc | |
|
ctLocSpan :: CtLoc -> RealSrcSpan Source #
ctLocLevel :: CtLoc -> TcLevel Source #
ctLocOrigin :: CtLoc -> CtOrigin Source #
ctLocDepth :: CtLoc -> SubGoalDepth Source #
bumpCtLocDepth :: CtLoc -> CtLoc Source #
isGivenLoc :: CtLoc -> Bool Source #
setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc Source #
data CtEvidence Source #
CtGiven | |
CtWanted | |
| |
CtDerived | |
|
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 are always HoleDest; other wanteds are always 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
mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc Source #
isWanted :: CtEvidence -> Bool Source #
isGiven :: CtEvidence -> Bool Source #
isDerived :: CtEvidence -> Bool Source #
ctEvRole :: CtEvidence -> Role Source #
Get the role relevant for a CtEvidence
data ShadowInfo Source #
Instances
Eq ShadowInfo Source # | |
Defined in GHC.Tc.Types.Constraint (==) :: ShadowInfo -> ShadowInfo -> Bool # (/=) :: ShadowInfo -> ShadowInfo -> 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.Monad
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
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool Source #
eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool Source #
eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool Source #
pprEvVarTheta :: [EvVar] -> SDoc Source #
pprEvVarWithType :: EvVar -> SDoc Source #