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

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 8174fa4 · 2026-10-11

Moduleghc-10.0.0.20260917GHC2024

GHC.HsToCore.Pmc.Solver.Types

Domain types used in GHC.HsToCore.Pmc.Solver. The ultimate goal is to define Nabla, which models normalised refinement types from the paper Lower Your Guards: A Compositional Pattern-Match Coverage Checker".

  • 14 types
  • 22 values

Normalised refinement types

10 declarations
datadata VarInfo
#

Information about an Id. Stores positive (vi_pos) facts, like x ~ Just 42, and negative (vi_neg) facts, like "x is not (:)". Also caches the type (vi_ty), the ResidualCompleteMatches of a COMPLETE set (vi_rcm).

Subject to Note [The Pos/Neg invariant] in GHC.HsToCore.Pmc.Solver.

Constructors

  • VI
    • vi_id :: !Id

      The Id in question. Important for adding new constraints relative to this VarInfo when we don't easily have the Id available.

    • vi_pos :: ![PmAltConApp]

      Positive info: PmAltCon apps it is (i.e. x ~ [Just y, PatSyn z]), all at the same time (i.e. conjunctive). We need a list because of nested pattern matches involving pattern synonym case x of { Just y -> case x of PatSyn z -> ... } However, no more than one RealDataCon in the list, otherwise contradiction because of generativity.

    • vi_neg :: !PmAltConSet

      Negative info: A list of PmAltCons that it cannot match. Example, assuming

          data T = Leaf Int | Branch T T | Node Int T

      then x ≁ [Leaf, Node] means that x cannot match a Leaf or Node, and hence can only match Branch. Is orthogonal to anything from vi_pos, in the sense that eqPmAltCon returns PossiblyOverlap for any pairing between vi_pos and vi_neg.

    • vi_bot :: BotInfo

      Can this variable be ⊥? Models (mutually contradicting) x ~ ⊥ and x ≁ ⊥ constraints. E.g. * MaybeBot: Don't know; Neither x ~ ⊥ nor x ≁ ⊥. * IsBot: x ~ ⊥ * IsNotBot: x ≁ ⊥

    • vi_rcm :: !ResidualCompleteMatches

      A cache of the associated COMPLETE sets. At any time a superset of possible constructors of each COMPLETE set. So, if it's not in here, we can't possibly match on it. Complementary to vi_neg. We still need it to recognise completion of a COMPLETE set efficiently for large enums.

Instances1Outputable
  • Outputable VarInfoDefined in ghc-10.0.0.20260917 · GHC.HsToCore.Pmc.Solver.Types

    Not user-facing.

datadata TmState
#

The term oracle state. Stores VarInfo for encountered Ids. These entries are possibly shared when we figure out that two variables must be equal, thus represent the same set of values.

See Note [TmState invariants] in GHC.HsToCore.Pmc.Solver.

Constructors

  • TmSt
    • ts_facts :: !UniqSDFM Id VarInfo

      Facts about term variables. Deterministic env, so that we generate deterministic error messages.

    • ts_reps :: !CoreMap Id

      An environment for looking up whether we already encountered semantically equivalent expressions that we want to represent by the same Id representative.

    • ts_dirty :: !DIdSet

      Which VarInfo needs to be checked for inhabitants because of new negative constraints (e.g. x ≁ ⊥ or x ≁ K).

Instances1Outputable
  • Outputable TmStateDefined in ghc-10.0.0.20260917 · GHC.HsToCore.Pmc.Solver.Types

    Not user-facing.

datadata TyState
#

The type oracle state. An GHC.Tc.Solver.Monad.InertSet that we incrementally add local type constraints to, together with a sequence number that counts the number of times we extended it with new facts.

Constructors

Instances1Outputable
  • Outputable TyStateDefined in ghc-10.0.0.20260917 · GHC.HsToCore.Pmc.Solver.Types

    Not user-facing.

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.

Constructors

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

Looking up VarInfo

valuelookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
#

Like lookupVarInfo ts x, but lookupVarInfo ts x = (y, vi) also looks through newtype constructors. We have x ~ N1 (... (Nk y)) such that the returned y doesn't have a positive newtype constructor constraint associated with it (yet). The VarInfo returned is that of y's representative.

Careful, this means that idType x might be different to idType y, even modulo type normalisation!

See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.

Caching residual COMPLETE sets

datadata ResidualCompleteMatches
#

A data type that caches for the VarInfo of x the results of querying dsGetCompleteMatches and then striking out all occurrences of K for which we already know x ≁ K from these sets.

For motivation, see Section 5.3 in Lower Your Guards. See also Note [Implementation of COMPLETE pragmas]

Constructors

  • RCM
    • rcm_vanilla :: !Maybe DsCompleteMatch

      The residual set for the vanilla COMPLETE set from the data defn. Tracked separately from rcm_pragmas, because it might only be known much later (when we have enough type information to see the TyCon of the match), or not at all even. Until that happens, it is Nothing.

    • rcm_pragmas :: !Maybe DsCompleteMatches

      The residual sets for all COMPLETE sets from pragmas that are visible when compiling this module. Querying that set with dsGetCompleteMatches requires DsM, so we initialise it with Nothing until first needed in a DsM context.

Instances1Outputable

Representations for Literals and AltCons

datadata PmLit
#

Literals (simple and overloaded ones) for pattern match checking.

See Note [Undecidable Equality for PmAltCons]

Constructors

Instances3Eq, Ord, Outputable
  • Eq PmLitDefined in ghc-10.0.0.20260917 · GHC.HsToCore.Pmc.Solver.Types

    Syntactic equality. We want (Ord PmLit) so that we can use (Set PmLit) in PmAltConSet

  • Ord PmLitDefined in ghc-10.0.0.20260917 · GHC.HsToCore.Pmc.Solver.Types
  • Outputable PmLitDefined in ghc-10.0.0.20260917 · GHC.HsToCore.Pmc.Solver.Types
valueisPmAltConMatchStrict :: PmAltCon -> Bool
#

Is a match on this constructor forcing the match variable? True of data constructors, literals and pattern synonyms (#17357), but not of newtypes. See Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.

PmAltConSet

Equality on PmAltCons

valueeqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
#

We can't in general decide whether two PmAltCons match the same set of values. In addition to the reasons in eqPmLit and eqConLike, a PmAltConLike might or might not represent the same value as a PmAltLit. See Note [Undecidable Equality for PmAltCons].

  • Just True ==> Surely equal

  • Just False ==> Surely different (non-overlapping, even!)

  • Nothing ==> Equality relation undecidable

Examples (omitting some constructor wrapping):

  • eqPmAltCon (LitInt 42) (LitInt 1) == Just False: Lit equality is decidable

  • eqPmAltCon (DataCon A) (DataCon B) == Just False: DataCon equality is decidable

  • eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing: OverLit equality is undecidable

  • eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing: PatSyn equality is undecidable

  • eqPmAltCon (DataCon I#) (LitInt 1) == Nothing: DataCon to Lit comparisons are undecidable without reasoning about the wrapped Int#

  • eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True: We assume reflexivity for overloaded literals

  • eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True: We assume reflexivity for Pattern Synonyms

Operations on PmLit