Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.
Synopsis
- type DsM = TcRnIf DsGblEnv DsLclEnv
- tracePm :: String -> SDoc -> DsM ()
- mkPmId :: Type -> DsM Id
- data Delta
- initDeltas :: Deltas
- lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
- lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [TyVar], [Id])
- data PmCt = PmTyCt !TyCt
- 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)
- canDiverge :: Delta -> Id -> Bool
- provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
Documentation
An inert set of canonical (i.e. mutually compatible) term and type constraints.
initDeltas :: Deltas Source #
An oracle constraint.
pattern PmNotBotCt :: Id -> PmCt Source #
canDiverge :: Delta -> Id -> Bool Source #
Check whether adding a constraint x ~ BOT
to Delta
succeeds.
provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta] Source #
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.