GHC.HsToCore.Pmc.Solver

Model refinements type as per the Lower Your Guards paper. The main export of the module are the functions addPhiCtsNablas for adding facts to the oracle, isInhabited to check if a refinement type is inhabited and generateInhabitingPatterns to turn a Nabla into a concrete pattern for an equation.

In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6 and 3.7. E.g., it represents refinement types directly as a bunch of normalised refinement types Nabla.

Documentation

data Nabla

A normalised refinement type ∇ ("nabla"), comprised of an inert set of canonical (i.e. mutually compatible) term and type constraints that form the refinement type's predicate.

Instances

Outputable Nabla

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: Nabla -> SDoc

newtype Nablas

A disjunctive bag of Nablas, representing a refinement type.

Constructors

MkNablas (Bag Nabla)

Instances

Monoid Nablas

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

mempty :: Nablas

mappend :: Nablas -> Nablas -> Nablas

mconcat :: [Nablas] -> Nablas

Semigroup Nablas

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

(<>) :: Nablas -> Nablas -> Nablas

sconcat :: NonEmpty Nablas -> Nablas

stimes :: Integral b => b -> Nablas -> Nablas

Outputable Nablas

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: Nablas -> SDoc

initNablas :: Nablas

lookupRefuts :: Nabla -> Id -> [PmAltCon]

lookupSolution :: Nabla -> Id -> Maybe PmAltConApp

data PhiCt

A high-level pattern-match constraint. Corresponds to φ from Figure 3 of the LYG paper.

Constructors

PhiTyCt !PredType

A type constraint "T ~ U".

PhiCoreCt !Id !CoreExpr

PhiCoreCt x e encodes "x ~ e", equating x with the CoreExpr e.

PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id]

PhiConCt x K tvs dicts ys encodes K @tvs dicts ys <- x, matching x against the PmAltCon application K @tvs dicts ys, binding tvs, dicts and possibly unlifted fields ys in the process. See Note [Strict fields and variables of unlifted type].

PhiNotConCt !Id !PmAltCon

PhiNotConCt x K encodes "x ≁ K", asserting that x can't be headed by K.

PhiBotCt !Id

PhiBotCt x encodes "x ~ ⊥", equating x to ⊥. by K.

PhiNotBotCt !Id

PhiNotBotCt x y encodes "x ≁ ⊥", asserting that x can't be ⊥.

Instances

Outputable PhiCt

Defined in GHC.HsToCore.Pmc.Solver

Methods

ppr :: PhiCt -> SDoc

type PhiCts = Bag PhiCt

addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas

addPmCtsNablas for a single PmCt.

addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas

Add a bunch of PhiCts to all the Nablas. Lifts addPhiCts over many Nablas.

isInhabited :: Nablas -> DsM Bool

Test if any of the Nablas is inhabited. Currently this is pure, because we preserve the invariant that there are no uninhabited Nablas. But that could change in the future, for example by implementing this function in terms of notNull $ generateInhabitingPatterns 1 ds.

generateInhabitingPatterns :: [Id] -> Int -> Nabla -> DsM [Nabla]

generateInhabitingPatterns vs n nabla returns a list of at most n (but perhaps empty) refinements of nabla that represent inhabited patterns. Negative information is only retained if literals are involved or for recursive GADTs.