HORIZON HASKELLDocslts/ghc-10.0.xaa25b892026-10-10Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · aa25b89 · 2026-10-10

Moduleghc-10.0.0.20260917GHC2024

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.

  • 5 types
  • 5 values
datadata 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.

Instances1Outputable
  • Outputable NablaDefined in ghc-10.0.0.20260917 · GHC.HsToCore.Pmc.Solver.Types
newtypenewtype Nablas
#

A disjunctive bag of Nablas, representing a refinement type.

Constructors

Instances5Generic, Semigroup, Monoid, Outputable, Rep
datadata 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 ⊥.

Instances1Outputable
valueisInhabited :: 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.