Safe Haskell | None |
---|---|
Language | GHC2021 |
Monadic definitions for the constraint solver
Synopsis
- data TcS a
- runTcS :: TcS a -> TcM (a, EvBindMap)
- runTcSEarlyAbort :: TcS a -> TcM a
- runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a
- runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
- failTcS :: TcRnMessage -> TcS a
- warnTcS :: TcRnMessage -> TcS ()
- addErrTcS :: TcRnMessage -> TcS ()
- wrapTcS :: TcM a -> TcS a
- ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
- runTcSEqualities :: TcS a -> TcM a
- nestTcS :: TcS a -> TcS a
- nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
- setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
- emitImplicationTcS :: TcLevel -> SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> Cts -> TcS TcEvBinds
- emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon -> [TcTyVar] -> Cts -> TcS ()
- emitFunDepWanteds :: CtEvidence -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool
- selectNextWorkItem :: TcS (Maybe Ct)
- getWorkList :: TcS WorkList
- updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
- pushLevelNoWorkList :: SDoc -> TcS a -> TcS (TcLevel, a)
- runTcPluginTcS :: TcPluginM a -> TcS a
- recordUsedGREs :: Bag GlobalRdrElt -> TcS ()
- matchGlobalInst :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
- data ClsInstResult
- = NoInstance
- | OneInst {
- cir_new_theta :: [TcPredType]
- cir_mk_ev :: [EvExpr] -> EvTerm
- cir_canonical :: Canonical
- cir_what :: InstanceWhat
- | NotSure
- data QCInst = QCI {
- qci_ev :: CtEvidence
- qci_tvs :: [TcTyVar]
- qci_pred :: TcPredType
- qci_pend_sc :: ExpansionFuel
- data StopOrContinue a
- = StartAgain Ct
- | ContinueWith !a
- | Stop CtEvidence SDoc
- continueWith :: a -> TcS (StopOrContinue a)
- stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
- startAgainWith :: Ct -> TcS (StopOrContinue a)
- newtype SolverStage a = Stage {
- runSolverStage :: TcS (StopOrContinue a)
- simpleStage :: TcS a -> SolverStage a
- stopWithStage :: CtEvidence -> String -> SolverStage a
- panicTcS :: SDoc -> TcS a
- traceTcS :: String -> SDoc -> TcS ()
- tryEarlyAbortTcS :: TcS ()
- traceFireTcS :: CtEvidence -> SDoc -> TcS ()
- bumpStepCountTcS :: TcS ()
- csTraceTcS :: SDoc -> TcS ()
- wrapErrTcS :: TcM a -> TcS a
- wrapWarnTcS :: TcM a -> TcS a
- resetUnificationFlag :: TcS Bool
- setUnificationFlag :: TcLevel -> TcS ()
- data MaybeNew
- freshGoals :: [MaybeNew] -> [CtEvidence]
- isFresh :: MaybeNew -> Bool
- getEvExpr :: MaybeNew -> EvExpr
- newTcEvBinds :: TcS EvBindsVar
- newNoTcEvBinds :: TcS EvBindsVar
- newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
- emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion
- newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew
- newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence
- newWantedEvVarNC :: CtLoc -> RewriterSet -> TcPredType -> TcS CtEvidence
- newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
- unifyTyVar :: TcTyVar -> TcType -> TcS ()
- reportUnifications :: TcS a -> TcS (Int, a)
- touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool
- setEvBind :: EvBind -> TcS ()
- setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS ()
- setWantedEvTerm :: TcEvDest -> Canonical -> EvTerm -> TcS ()
- setEvBindIfWanted :: CtEvidence -> Canonical -> EvTerm -> TcS ()
- newEvVar :: TcPredType -> TcS EvVar
- newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
- emitNewGivens :: CtLoc -> [(Role, TcType, TcType, TcCoercion)] -> TcS ()
- checkReductionDepth :: CtLoc -> TcType -> TcS ()
- getSolvedDicts :: TcS (DictMap DictCt)
- setSolvedDicts :: DictMap DictCt -> TcS ()
- getInstEnvs :: TcS InstEnvs
- getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
- getTopEnv :: TcS HscEnv
- getGblEnv :: TcS TcGblEnv
- getLclEnv :: TcS TcLclEnv
- setSrcSpan :: RealSrcSpan -> TcS a -> TcS a
- getTcEvBindsVar :: TcS EvBindsVar
- getTcLevel :: TcS TcLevel
- getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
- getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
- setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
- tcLookupClass :: Name -> TcS Class
- tcLookupId :: Name -> TcS Id
- tcLookupTyCon :: Name -> TcS TyCon
- updInertSet :: (InertSet -> InertSet) -> TcS ()
- updInertCans :: (InertCans -> InertCans) -> TcS ()
- getHasGivenEqs :: TcLevel -> TcS (HasGivenEqs, InertIrreds)
- setInertCans :: InertCans -> TcS ()
- getInertEqs :: TcS InertEqs
- getInertCans :: TcS InertCans
- getInertGivens :: TcS [Ct]
- getInertInsols :: TcS Cts
- getInnermostGivenEqLevel :: TcS TcLevel
- getInertSet :: TcS InertSet
- setInertSet :: InertSet -> TcS ()
- getUnsolvedInerts :: TcS (Bag Implication, Cts)
- removeInertCts :: [Ct] -> InertCans -> InertCans
- getPendingGivenScs :: TcS [Ct]
- insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
- addInertForAll :: QCInst -> TcS ()
- emitWorkNC :: [CtEvidence] -> TcS ()
- emitWork :: Cts -> TcS ()
- lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
- kickOutAfterUnification :: [TcTyVar] -> TcS ()
- kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS ()
- addInertSafehask :: InertCans -> DictCt -> InertCans
- insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
- updInertSafehask :: (DictMap DictCt -> DictMap DictCt) -> TcS ()
- getSafeOverlapFailures :: TcS (Bag DictCt)
- updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
- lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
- foldIrreds :: (IrredCt -> b -> b) -> InertIrreds -> b -> b
- lookupFamAppInert :: (CtFlavourRole -> Bool) -> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
- lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
- extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
- pprKicked :: Int -> SDoc
- instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
- wrapUnifierTcS :: CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Bag Ct, [TcTyVar])
- unifyFunDeps :: CtEvidence -> Role -> (UnifyEnv -> TcM ()) -> TcS Bool
- uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
- unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts)
- newFlexiTcSTy :: Kind -> TcS TcType
- instFlexiX :: Subst -> [TKVar] -> TcS Subst
- cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
- tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar])
- data TcLevel
- isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
- isFilledMetaTyVar :: TcTyVar -> TcS Bool
- isUnfilledMetaTyVar :: TcTyVar -> TcS Bool
- zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
- zonkTcType :: TcType -> TcS TcType
- zonkTcTypes :: [TcType] -> TcS [TcType]
- zonkTcTyVar :: TcTyVar -> TcS TcType
- zonkCo :: Coercion -> TcS Coercion
- zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
- zonkSimples :: Cts -> TcS Cts
- zonkWC :: WantedConstraints -> TcS WantedConstraints
- zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
- newTcRef :: a -> TcS (TcRef a)
- readTcRef :: TcRef a -> TcS a
- writeTcRef :: TcRef a -> a -> TcS ()
- updTcRef :: TcRef a -> (a -> a) -> TcS ()
- getDefaultInfo :: TcS ([Type], (Bool, Bool))
- getDynFlags :: HasDynFlags m => m DynFlags
- getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
- matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN)
- matchFamTcM :: TyCon -> [Type] -> TcM (Maybe ReductionN)
- checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
- pprEq :: TcType -> TcType -> SDoc
- checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType -> TcS (PuResult () Reduction)
- checkTouchableTyVarEq :: CtEvidence -> TcTyVar -> TcType -> TcS (PuResult () Reduction)
Documentation
Instances
MonadIO TcS Source # | |
HasDynFlags TcS Source # | |
Defined in GHC.Tc.Solver.Monad | |
MonadThings TcS Source # | |
MonadUnique TcS Source # | |
Defined in GHC.Tc.Solver.Monad getUniqueSupplyM :: TcS UniqSupply Source # getUniqueM :: TcS Unique Source # getUniquesM :: TcS [Unique] Source # | |
HasModule TcS Source # | |
Applicative TcS Source # | |
Functor TcS Source # | |
Monad TcS Source # | |
MonadFail TcS Source # | |
Defined in GHC.Tc.Solver.Monad | |
MonadFix TcS Source # | |
Defined in GHC.Tc.Solver.Monad |
runTcSEarlyAbort :: TcS a -> TcM a Source #
This variant of runTcS
will immediately fail upon encountering an
insoluble ct. See Note [Speeding up valid hole-fits]. Its one usage
site does not need the ev_binds, so we do not return them.
runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a Source #
failTcS :: TcRnMessage -> TcS a Source #
warnTcS :: TcRnMessage -> TcS () Source #
addErrTcS :: TcRnMessage -> TcS () Source #
ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS () Source #
runTcSEqualities :: TcS a -> TcM a Source #
This can deal only with equality constraints.
nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a Source #
setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a Source #
emitImplicationTcS :: TcLevel -> SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> Cts -> TcS TcEvBinds Source #
emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon -> [TcTyVar] -> Cts -> TcS () Source #
emitFunDepWanteds :: CtEvidence -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool Source #
runTcPluginTcS :: TcPluginM a -> TcS a Source #
recordUsedGREs :: Bag GlobalRdrElt -> TcS () Source #
matchGlobalInst :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS ClsInstResult Source #
data ClsInstResult Source #
NoInstance | |
OneInst | |
| |
NotSure |
Instances
Outputable ClsInstResult Source # | |
Defined in GHC.Tc.Instance.Class ppr :: ClsInstResult -> SDoc Source # |
QCI | |
|
Instances
data StopOrContinue a Source #
Instances
Functor StopOrContinue Source # | |
Defined in GHC.Tc.Solver.Monad fmap :: (a -> b) -> StopOrContinue a -> StopOrContinue b # (<$) :: a -> StopOrContinue b -> StopOrContinue a # | |
Outputable a => Outputable (StopOrContinue a) Source # | |
Defined in GHC.Tc.Solver.Monad ppr :: StopOrContinue a -> SDoc Source # |
continueWith :: a -> TcS (StopOrContinue a) Source #
stopWith :: CtEvidence -> String -> TcS (StopOrContinue a) Source #
startAgainWith :: Ct -> TcS (StopOrContinue a) Source #
newtype SolverStage a Source #
Stage | |
|
Instances
Applicative SolverStage Source # | |
Defined in GHC.Tc.Solver.Monad pure :: a -> SolverStage a # (<*>) :: SolverStage (a -> b) -> SolverStage a -> SolverStage b # liftA2 :: (a -> b -> c) -> SolverStage a -> SolverStage b -> SolverStage c # (*>) :: SolverStage a -> SolverStage b -> SolverStage b # (<*) :: SolverStage a -> SolverStage b -> SolverStage a # | |
Functor SolverStage Source # | |
Defined in GHC.Tc.Solver.Monad fmap :: (a -> b) -> SolverStage a -> SolverStage b # (<$) :: a -> SolverStage b -> SolverStage a # | |
Monad SolverStage Source # | |
Defined in GHC.Tc.Solver.Monad (>>=) :: SolverStage a -> (a -> SolverStage b) -> SolverStage b # (>>) :: SolverStage a -> SolverStage b -> SolverStage b # return :: a -> SolverStage a # |
simpleStage :: TcS a -> SolverStage a Source #
stopWithStage :: CtEvidence -> String -> SolverStage a Source #
tryEarlyAbortTcS :: TcS () Source #
traceFireTcS :: CtEvidence -> SDoc -> TcS () Source #
bumpStepCountTcS :: TcS () Source #
csTraceTcS :: SDoc -> TcS () Source #
wrapErrTcS :: TcM a -> TcS a Source #
wrapWarnTcS :: TcM a -> TcS a Source #
setUnificationFlag :: TcLevel -> TcS () Source #
freshGoals :: [MaybeNew] -> [CtEvidence] Source #
newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) Source #
Create a new Wanted constraint holding a coercion hole
for an equality between the two types at the given Role
.
emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion Source #
Emit a new Wanted equality into the work-list
newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew Source #
Create a new Wanted constraint, potentially looking up non-equality constraints in the cache instead of creating a new one from scratch.
Deals with both equality and non-equality constraints.
newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence Source #
Create a new Wanted constraint.
Deals with both equality and non-equality constraints.
Does not attempt to re-use non-equality constraints that already exist in the inert set.
newWantedEvVarNC :: CtLoc -> RewriterSet -> TcPredType -> TcS CtEvidence Source #
Create a new Wanted constraint holding an evidence variable.
Don't use this for equality constraints: use newWantedEq
instead.
newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar Source #
Make a new Id
of the given type, bound (in the monad's EvBinds) to the
given term
setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS () Source #
Equalities only
setWantedEvTerm :: TcEvDest -> Canonical -> EvTerm -> TcS () Source #
Good for both equalities and non-equalities
setEvBindIfWanted :: CtEvidence -> Canonical -> EvTerm -> TcS () Source #
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence Source #
emitNewGivens :: CtLoc -> [(Role, TcType, TcType, TcCoercion)] -> TcS () Source #
Checks if the depth of the given location is too much. Fails if it's too big, with an appropriate error message.
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) Source #
setSrcSpan :: RealSrcSpan -> TcS a -> TcS a Source #
getTcLevel :: TcS TcLevel Source #
getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap Source #
setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS () Source #
getHasGivenEqs :: TcLevel -> TcS (HasGivenEqs, InertIrreds) Source #
setInertCans :: InertCans -> TcS () Source #
getInertGivens :: TcS [Ct] Source #
getInertInsols :: TcS Cts Source #
Retrieves all insoluble constraints from the inert set, specifically including Given constraints.
This consists of:
- insoluble equalities, such as
Int ~# Bool
; - constraints that are top-level custom type errors, of the form
TypeError msg
, but not constraints such asEq (TypeError msg)
in which the type error is nested; - unsatisfiable constraints, of the form
Unsatisfiable msg
.
The inclusion of Givens is important for pattern match warnings, as we want to consider a pattern match that introduces insoluble Givens to be redundant (see Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver).
setInertSet :: InertSet -> TcS () Source #
getUnsolvedInerts :: TcS (Bag Implication, Cts) Source #
removeInertCts :: [Ct] -> InertCans -> InertCans Source #
Remove inert constraints from the InertCans
, for use when a
typechecker plugin wishes to discard a given.
getPendingGivenScs :: TcS [Ct] Source #
addInertForAll :: QCInst -> TcS () Source #
emitWorkNC :: [CtEvidence] -> TcS () Source #
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt Source #
Look up a dictionary inert.
kickOutAfterUnification :: [TcTyVar] -> TcS () Source #
kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS () Source #
insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS () Source #
updSolvedDicts :: InstanceWhat -> DictCt -> TcS () Source #
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence Source #
Look up a solved inert.
foldIrreds :: (IrredCt -> b -> b) -> InertIrreds -> b -> b Source #
lookupFamAppInert :: (CtFlavourRole -> Bool) -> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) Source #
Looks up a family application in the inerts.
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType) Source #
unifyFunDeps :: CtEvidence -> Role -> (UnifyEnv -> TcM ()) -> TcS Bool Source #
unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts) Source #
tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar]) Source #
writeTcRef :: TcRef a -> a -> TcS () Source #
getDynFlags :: HasDynFlags m => m DynFlags Source #
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe ReductionN) Source #
checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS () Source #
checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType -> TcS (PuResult () Reduction) Source #
checkTouchableTyVarEq :: CtEvidence -> TcTyVar -> TcType -> TcS (PuResult () Reduction) Source #