ghc-lib-parser-9.12.2.20250421: The GHC API, decoupled from GHC versions

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
- 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_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
  - = 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
- 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
  - = TyVarLHS TcTyVar
  - | TyFamLHS TyCon [Xi]
- canEqLHS_maybe :: Xi -> Maybe CanEqLHS
- canTyFamEqLHS_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 IrredCt -> 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
- insolubleCt :: Ct -> Bool
- insolubleIrredCt :: IrredCt -> 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 :: !CtLocEnv
  - ic_wanted :: WantedConstraints
  - ic_binds :: EvBindsVar
  - ic_need_inner :: VarSet
  - ic_need_outer :: VarSet
  - 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 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 {
    - 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
- 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
  - = 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 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 DictCt |
CIrredCan IrredCt |
CEqCan EqCt |
CQuantCan QCInst |
CNonCanonical CtEvidence |

#### Instances

Instances details

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

type Cts = Bag Ct 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 #

emptyCts :: Cts Source #

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

ctsPreds :: Cts -> [PredType] Source #

isPendingScDictCt :: DictCt -> 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 #

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 #

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 #

mkGivens :: CtLoc -> [EvId] -> [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 #

data EqCt Source #

Constructors

EqCt |

Fields

- eq_ev :: CtEvidence
- eq_lhs :: CanEqLHS
- eq_rhs :: Xi
- eq_eq_rel :: EqRel

#### Instances

Instances details

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

eqCtEvidence :: EqCt -> CtEvidence Source #

eqCtLHS :: EqCt -> CanEqLHS Source #

data DictCt Source #

Constructors

DictCt |

Fields

- di_ev :: CtEvidence
- di_cls :: Class
- di_tys :: [Xi]
- di_pend_sc :: ExpansionFuel

#### Instances

Instances details

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

dictCtEvidence :: DictCt -> CtEvidence Source #

dictCtPred :: DictCt -> TcPredType Source #

data IrredCt Source #

Constructors

IrredCt |

Fields

- ir_ev :: CtEvidence
- ir_reason :: CtIrredReason

#### Instances

Instances details

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

irredCtEvidence :: IrredCt -> CtEvidence Source #

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

ctIrredCt :: CtIrredReason -> Ct -> IrredCt Source #

irredCtPred :: IrredCt -> PredType Source #

data QCInst Source #

Constructors

QCI |

Fields

- qci_ev :: CtEvidence
- qci_tvs :: [TcTyVar]
- qci_pred :: TcPredType
- qci_pend_sc :: ExpansionFuel

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

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

#### Instances

Instances details

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

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 #

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

cteConcrete :: CheckTyEqProblem Source #

cteSkolemEscape :: CheckTyEqProblem Source #

impredicativeProblem :: CheckTyEqResult Source #

insolubleOccursProblem :: CheckTyEqResult Source #

solubleOccursProblem :: CheckTyEqResult Source #

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

cterHasOnlyProblems :: CheckTyEqResult -> CheckTyEqResult -> Bool Source #

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

  TyCon of the family

- [Xi]

  Arguments, 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.

canTyFamEqLHS_maybe :: Xi -> Maybe CanEqLHS Source #

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 `CanEqLHS`s 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 #

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

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.

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 :: !CtLocEnv
- 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 :: CtLocEnv -> 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 Source # (/=) :: HasGivenEqs -> HasGivenEqs -> Bool Source #

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

data CtLocEnv Source #

Local typechecker environment for a constraint.

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

See also `TcLclCtxt`.

Constructors

CtLocEnv |

Fields

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

setCtLocEnvLoc :: CtLocEnv -> SrcSpan -> CtLocEnv Source #

setCtLocEnvLvl :: CtLocEnv -> TcLevel -> CtLocEnv Source #

getCtLocEnvLoc :: CtLocEnv -> RealSrcSpan Source #

getCtLocEnvLvl :: CtLocEnv -> TcLevel Source #

ctLocEnvInGeneratedCode :: CtLocEnv -> Bool 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 #

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

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 #

addRewriter :: RewriterSet -> CoercionHole -> RewriterSet Source #

unitRewriterSet :: CoercionHole -> RewriterSet Source #

unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet Source #

rewriterSetFromCts :: Bag Ct -> 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 Source # (/=) :: CtFlavour -> CtFlavour -> Bool 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`

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

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

pprEvVarTheta :: [EvVar] -> SDoc Source #

pprEvVars :: [EvVar] -> SDoc Source #

pprEvVarWithType :: EvVar -> SDoc Source #