GHC.Tc.Solver.InertSet

The work list

data WorkList

Constructors

WL

Fields

• wl_eqs :: [Ct]
• wl_rw_eqs :: [Ct]
• wl_rest :: [Ct]
• wl_implics :: Bag Implication

Instances

Outputable WorkList

Defined in GHC.Tc.Solver.InertSet

Methods

ppr :: WorkList -> SDoc

isEmptyWorkList :: WorkList -> Bool

emptyWorkList :: WorkList

extendWorkListNonEq :: Ct -> WorkList -> WorkList

extendWorkListCt :: Ct -> WorkList -> WorkList

extendWorkListCts :: Cts -> WorkList -> WorkList

extendWorkListCtList :: [Ct] -> WorkList -> WorkList

extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList

extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList

appendWorkList :: WorkList -> WorkList -> WorkList

extendWorkListImplic :: Implication -> WorkList -> WorkList

workListSize :: WorkList -> Int

selectWorkItem :: WorkList -> Maybe (Ct, WorkList)

The inert set

data InertSet

Constructors

IS

Fields

• inert_cans :: InertCans
• inert_cycle_breakers :: CycleBreakerVarStack
• inert_famapp_cache :: FunEqMap Reduction
• inert_solved_dicts :: DictMap DictCt

Instances

Outputable InertSet

Defined in GHC.Tc.Solver.InertSet

Methods

ppr :: InertSet -> SDoc

data InertCans

Constructors

IC

Fields

• inert_eqs :: InertEqs
• inert_funeqs :: InertFunEqs
• inert_dicts :: DictMap DictCt
• inert_insts :: [QCInst]
• inert_safehask :: DictMap DictCt

  See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver

• inert_irreds :: InertIrreds
• inert_given_eq_lvl :: TcLevel
• inert_given_eqs :: Bool

Instances

Outputable InertCans

Defined in GHC.Tc.Solver.InertSet

Methods

ppr :: InertCans -> SDoc

emptyInert :: InertSet

noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool

Returns True iff there are no Given constraints that might, potentially, match the given class constraint. This is used when checking to see if a Given might overlap with an instance. See Note [Instance and Given overlap] in GHC.Tc.Solver.Dict

noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool

updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans

mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst

prohibitedSuperClassSolve

Arguments

:: CtLoc

is it loopy to use this one ...

-> CtLoc

... to solve this one?

-> Bool

True ==> don't solve it

Is it (potentially) loopy to use the first ct1 to solve ct2?

Necessary (but not sufficient) conditions for this function to return True:

• ct1 and ct2 both arise from superclass expansion,
• ct1 is a Given and ct2 is a Wanted.

See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2).

Inert equalities

type InertEqs = DTyVarEnv EqualCtList

foldTyEqs :: (EqCt -> b -> b) -> InertEqs -> b -> b

delEq :: EqCt -> InertCans -> InertCans

findEq :: InertCans -> CanEqLHS -> [EqCt]

partitionInertEqs :: (EqCt -> Bool) -> InertEqs -> ([EqCt], InertEqs)

partitionFunEqs :: (EqCt -> Bool) -> InertFunEqs -> ([EqCt], InertFunEqs)

foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b

addEqToCans :: TcLevel -> EqCt -> InertCans -> InertCans

Inert Dicts

updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans

delDict :: DictCt -> DictMap a -> DictMap a

addDict :: DictCt -> DictMap DictCt -> DictMap DictCt

filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt

partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)

addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt

Inert Irreds

type InertIrreds = Bag IrredCt

delIrred :: IrredCt -> InertCans -> InertCans

addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds

addIrred :: IrredCt -> InertIrreds -> InertIrreds

foldIrreds :: (IrredCt -> b -> b) -> InertIrreds -> b -> b

findMatchingIrreds :: InertIrreds -> CtEvidence -> (Bag (IrredCt, SwapFlag), InertIrreds)

updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans

addIrredToCans :: TcLevel -> IrredCt -> InertCans -> InertCans

Kick-out

data KickOutSpec

Constructors

KOAfterUnify TcTyVarSet

KOAfterAdding CanEqLHS

kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Cts, InertCans)

Cycle breaker vars

type CycleBreakerVarStack

Arguments

 = NonEmpty (Bag (TcTyVar, TcType))

a stack of (CycleBreakerTv, original family applications) lists first element in the stack corresponds to current implication; later elements correspond to outer implications used to undo the cycle-breaking needed to handle Note [Type equality cycles] in GHC.Tc.Solver.Equality Why store the outer implications? For the use in mightEqualLater (only)

Why NonEmpty? So there is always a top element to add to

pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack

Push a fresh environment onto the cycle-breaker var stack. Useful when entering a nested implication.

addCycleBreakerBindings

Arguments

:: Bag (TcTyVar, Type)

(cbv,expansion) pairs

-> InertSet

-> InertSet

Add a new cycle-breaker binding to the top environment on the stack.

forAllCycleBreakerBindings_ :: Monad m => CycleBreakerVarStack -> (TcTyVar -> TcType -> m ()) -> m ()

Perform a monadic operation on all pairs in the top environment in the stack.

Solving one from another

data InteractResult

Constructors

KeepInert

KeepWork

Instances

Outputable InteractResult

Defined in GHC.Tc.Solver.InertSet

Methods

ppr :: InteractResult -> SDoc

solveOneFromTheOther :: Ct -> Ct -> InteractResult