GHC.HsToCore.PmCheck.Oracle

The pattern match oracle. The main export of the module are the functions addPmCts for adding facts to the oracle, and provideEvidence to turn a Delta into a concrete evidence for an equation.

Documentation

type DsM = TcRnIf DsGblEnv DsLclEnv

tracePm :: String -> SDoc -> DsM ()

mkPmId :: Type -> DsM Id

Generate a fresh Id of a given type

data Delta

An inert set of canonical (i.e. mutually compatible) term and type constraints.

Instances

Outputable Delta

Defined in GHC.HsToCore.PmCheck.Types

Methods

ppr :: Delta -> SDoc

pprPrec :: Rational -> Delta -> SDoc

initDeltas :: Deltas

lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]

lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [TyVar], [Id])

data PmCt

An oracle constraint.

Constructors

PmTyCt !TyCt

PmTy pred_ty carries PredTypes, for example equality constraints.

Instances

Outputable PmCt

Defined in GHC.HsToCore.PmCheck.Oracle

Methods

ppr :: PmCt -> SDoc

pprPrec :: Rational -> PmCt -> SDoc

type PmCts = Bag PmCt

pattern PmVarCt :: Id -> Id -> PmCt

pattern PmCoreCt :: Id -> CoreExpr -> PmCt

pattern PmConCt :: Id -> PmAltCon -> [TyVar] -> [Id] -> PmCt

pattern PmNotConCt :: Id -> PmAltCon -> PmCt

pattern PmBotCt :: Id -> PmCt

pattern PmNotBotCt :: Id -> PmCt

addPmCts :: Delta -> PmCts -> DsM (Maybe Delta)

Adds new constraints to Delta and returns Nothing if that leads to a contradiction.

canDiverge :: Delta -> Id -> Bool

Check whether adding a constraint x ~ BOT to Delta succeeds.

provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]

provideEvidence vs n delta returns a list of at most n (but perhaps empty) refinements of delta that instantiate vs to compatible constructor applications or wildcards. Negative information is only retained if literals are involved or when for recursive GADTs.