Keys, Canonicalization, and Reification

This module is responsible for converting class applications of any kind into Vertexs or Keys, which is the process we refer to as canonicalization, and back, which we refer to as reification.

Main definitions:

• keySlots tries to figure out what parameter "slots" of a class are recoverable from the others, which are slots that we don't want to index our class graph with. For instance, for Module R M inst₁ inst₂, the key slots are the first two parameter slots (corresponding to R and M).
• canonArg canonicalizes a single argument. For example, for Module R M, this means R and M become #0 and #1. For Pow α ℕ, this means α becomes #0 and ℕ remains ℕ.
• canonKey canonicalizes a class application into a Key that we query the class graph with.
• mkClassApp? takes a class name and its key arguments, and reifies them into a proper class application.
• reifyKey? takes a class name and a pattern and corresponding subst, and reifies them into a proper class application.

Head Helpers

def GeneralizationLinter.isTypeFormerConst (env : Lean.Environment) (e : Lean.Expr) : Bool

isTypeFormerConst e is true iff e is a (possibly nullary) type former constant, i.e., a constant whose type ends in a Sort.

---

Examples

isTypeFormerConst returns true on the following:

• Nullary type formers: Nat, etc.
• Unary type formers: Group, List, etc.
• Binary type formers: Prod, And, etc.
• etc.

isTypeFormerConst returns false on the following:

• Constants that are not type formers: And.intro, Nat.succ, etc.
• Things that are not constants: 3, #[3], {}, [], etc.

Equations

• GeneralizationLinter.isTypeFormerConst env (Lean.Expr.const c us) = Option.any (fun (x : Lean.ConstantInfo) => x.type.getForallBody.isSort) (env.find? c)
• GeneralizationLinter.isTypeFormerConst env e = false

def GeneralizationLinter.declStamp (n : Lean.Name) : Lean.MetaM UInt64

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.isSynonymFormer (h : Lean.Name) : Lean.MetaM Bool

Is h a "synonym type former", i.e., a former that unfolds to one of its own arguments.

---

Examples

isSynonymFormer `Monoid = false
isSynonymFormer `OrderDual = true

Equations

• One or more equations did not get rendered due to their size.

Key Arguments

def GeneralizationLinter.keySlots (head : Lean.Name) : Lean.MetaM (Array Bool)

Given a head constant head, return a boolean mask #[b₁ … bₙ] (bᵢ : Bool) such that bᵢ is true iff the ith slot of head is one that should be kept when converting an application of head into a Key or into an entry of a different Key's pattern. Note that keySlots is used not only for classes, but for all kinds of type formers.

Instance implicit slots are always dropped, while other slots are dropped only if their values are recoverable from the values of the kept slots.

The two drops rest on different grounds: a non-instance slot is dropped because unification recovers it (see recoverableFrom), an instance slot because mkClassApp? re-synthesizes it, which can fail, and which agrees with the original only under instance coherence. Instance slots are also kept out of recoverableFrom's pool: their types mention the carriers, so admitting them would make each carrier look recoverable (pinned by its own instance argument) and drop it out of the key.

keySlotsCacheRef memoizes by declStamp, so an edited declaration gets a fresh mask. Marking a definition irreducible mid-session can still leave a stale one, since recoverableFrom reduces and the stamp does not see transparency. No caller varies transparency today.

---

Examples

-- class Module (R M : Type*) [Semiring R] [AddCommMonoid M]
keySlots `Module = #[true, true, false, false]
-- class Small (α : Type*)
keySlots `Small = #[true]
-- structure Subtype {α : Sort u} (p : α → Prop)
keySlots `Subtype = #[false, true]
-- class IsWellFounded (α : Type*) (r : α → α → Prop)
keySlots `IsWellFounded = #[false, true]
-- structure Submodule (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
keySlots `Submodule = #[true, true, false, false, false]

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.keyArgs (fn : Lean.Expr) (vals : Array Lean.Expr) : Lean.MetaM (Array Lean.Expr)

The key arguments of an application fn a₁ … aₙ (vals = #[a₁, …, aₙ]), in accordance with keySlots applied to fn's head constant. If fn isn't a constant, all of vals is kept.

---

Examples

-- class Module (R M : Type*) [Semiring R] [AddCommMonoid M]
keyArgs ‹Module› #[R, M, inst₁, inst₂] = #[R, M]
-- structure Subtype {α : Sort u} (p : α → Prop)
keyArgs ‹Subtype› #[α, p] = #[p]
-- `f` a free variable
keyArgs ‹f› #[a, b] = #[a, b]

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.eraseConstLevels : Lean.Expr → Lean.Expr

Used to strip the universe-level arguments off the heads of type formers used within a key slot. We delegate all handling of universe levels to Vertex.levels.

Equations

• GeneralizationLinter.eraseConstLevels (Lean.Expr.const c us) = Lean.Expr.const c []
• GeneralizationLinter.eraseConstLevels x✝ = x✝

def GeneralizationLinter.natLitOf? : Lean.Expr → Option Nat

Retrieves the value of a Nat-valued argument.

---

Examples

• .lit (.natVal n) → some n
• @OfNat.ofNat ℕ n _ → some n

Canonicalization

@[reducible, inline]

abbrev GeneralizationLinter.CanonVarsM (α : Type) : Type

As we walk an Expr (generally, a telescope), this monad helps us keep track of two things:

• HashMap FVarId Nat: For each fvar id (where id is some FVarId) that we canonicalize as a whole argument, we add an entry id → k to this map to note to which canonical bvar k we've mapped fvar id.
• Array Expr: This keeps track of the specific carriers we've collected thus far, ordered by their de Bruijn indices.

Invariant: The size of the Array is always greater than or equal to the size of the HashMap.

Equations

• GeneralizationLinter.CanonVarsM = StateT (Std.HashMap Lean.FVarId Nat × Array Lean.Expr) Lean.MetaM

partial def GeneralizationLinter.canonArg (e : Lean.Expr) : CanonVarsM Lean.Expr

Canonicalize a single binder/argument.

---

Examples

• ℕ → ℕ
• 3 → 3
• Group G → Group #0
• Module R R → Module #0 #0
• Pow α ℕ → Pow #0 ℕ
• OfNat α 1 → OfNat #0 1

def GeneralizationLinter.universeLevelsOf (lvls : List Lean.Level) : UniverseLevels

Canonicalized universe arguments for a head with universe arguments lvls.

• concrete: when there are no universe parameters or metavariables; in other words, when the class application is not universe-polymorphic. In this case, we track the specific universe levels of the class application.
• polymorphic: when the class application is universe-polymorphic. In this case, we don't track the universe levels, so we "erase" that information.

---

Examples

universeLevelsOf [0, 1] = .concrete #[0, 1]
universeLevelsOf [u]    = .polymorphic     -- `u` is a universe variable
universeLevelsOf []     = .concrete #[]    -- monomorphic class, e.g., `Fact`

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.canonKey (e : Lean.Expr) : Lean.MetaM Key

Given an Expr of a class application, canonicalize it into a Key.

---

Implementation notes

• The head name (which sets Vertex.name) and canonicalized arguments (which set Vertex.pattern) are taken from the whnfR form of the expression, so for example IsNoetherianRing R, which reduces to IsNoetherian R R, would have Vertex.name := ``IsNoetherian and Vertex.pattern := #[.bvar 0, .bvar 0].
• For a parametric class binder like ∀ prefix, C args, the body (C args) determines the Vertex fields, while the parametric index in the prefix is abstracted to a bvar. So, for example, for [∀ i : ι, Monoid (f i)], where f : ι → Type* is some free variable, we'd have name := `Monoid, pattern := #[.bvar 0], subst := #[f (.bvar 0)], and forallArity := 1.
• If the body of such a Π-binder doesn't canonicalize to a constant-headed application (so the head name would come out .anonymous), we instead canonicalize the whole Π-expression as one opaque carrier. For ∀ n : ℕ, P n, with P a free variable, this yields name := .anonymous, pattern := #[], subst := #[∀ n : ℕ, P n], and forallArity := 0.

---

Examples

-- class Module (R M : Type*) [Semiring R] [AddCommMonoid M]
canonKey ‹@Module R M inst₁ inst₂› = {
  -- `Vertex` fields
  name := `Module,
  levels := .polymorphic
  pattern := #[.bvar 0, .bvar 1],
  -- `Key` fields
  subst := #[R, M],
  forallArity := 0,
}

-- class Small (α : Type*)
-- structure Subtype {α : Sort u} (p : α → Prop)
canonKey ‹@Small (@Subtype α p)› = {
  -- `Vertex` fields
  name := `Small,
  levels := .polymorphic
  pattern := #[Subtype (.bvar 0)],
  -- `Key` fields
  subst := #[p],
  forallArity := 0,
}

-- Let `f` be a free variable with `f : ι → Type*`.
canonKey ‹∀ i : ι, Monoid (f i)› = {
  -- `Vertex` fields
  name := `Monoid,
  levels := .polymorphic
  pattern := #[.bvar 0],
  -- `Key` fields
  subst := #[f (.bvar 0)]
  forallArity := 1,
}

Note how the class application Small (Subtype p) gets indexed in the class graph in accordance with what keySlots returns for the type former Subtype, which is not itself a class.

Equations

• One or more equations did not get rendered due to their size.

Reification

def GeneralizationLinter.mkClassApp? (name : Lean.Name) (vals : Array Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Reifies a class name at its key arguments vals (see keySlots) into a valid Expr, wrapped as an Option (none if name is not a constant defined in the environment, or if the application could not be built). Note that a synthesis exception propagates rather than becoming none.

---

Example

Suppose the linter encountered the following declaration, and that Algebra could be weakened to Module within this declaration.

theorem thm.{w} {S : Type 0} {A : Type w} [CommSemiring S] [Semiring A] [Algebra S A] (x : A) : … := …

To know what exactly it'd be suggesting (e.g., so that it can verify said suggestion candidate), the linter needs to construct the weakened binder's type, Module S A. To do this, it calls replaceBinderType? with Algebra S A as an Expr and the replacement Vertex for Module S A. This in turn then computes the key of Algebra S A (which has subst = #[S, A]), and then calls reifyKey? `Module #[.bvar 0, .bvar 1] #[S, A], which then calls mkClassApp? `Module #[S, A], which will in turn output the Expr corresponding to Module S A (wrapped as an Option; if `Module were not a constant defined in the environment, mkClassApp? would return none).

Note that, in constructing its output, mkClassApp? may perform instance synthesis: in the `Module example, it's actually constructing @Module S A ?i₁ ?i₂, and finds ?i₁ and ?i₂ (instance metavariables spawned by mkClassApp?) via instance synthesis.

Equations

• One or more equations did not get rendered due to their size.

partial def GeneralizationLinter.reifyArg? (e : Lean.Expr) (subst : Array Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Essentially the inverse of canonArg.

Here, e is a pattern entry of a class graph vertex v : Vertex and reifyArg? e subst is tasked with reifying this e using the subst field of some key k : Key for which k.toVertex = v. In the vast majority of cases, e is just a plain bvar and reifyArg? just returns the corresponding subst entry. However, if e is a constant-headed, non-nullary application, it'll return e re-elaborated (i.e., with the non-key args which canonArg dropped inferred back, and fresh universe levels applied and determined, since canonArg erases universe levels too) with any bvars in any of its arguments replaced using subst.

---

Examples

reifyArg? ‹#0› #[α] = some ‹α›
reifyArg? ‹#0› #[Fintype.card α] = some ‹Fintype.card α›
reifyArg? ‹Int› #[] = some ‹Int›
reifyArg? ‹42› #[] = some ‹42›
reifyArg? ‹Units #0› #[α] = some ‹Units α›
reifyArg? ‹Subtype #0› #[p] = some ‹@Subtype α p›

def GeneralizationLinter.reifyKey? (name : Lean.Name) (pattern subst : Array Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Essentially the inverse of canonKey for non-parametric class binders. Reifies the class name by instantiating the pattern of its key with the concrete values provided by subst, each elaborated against the corresponding slot's expected type, and then inferring the non-key-slots of name. Returns none if pattern needs more values than subst provides, or if elaboration or inference failed at any point.

---

Example

-- class Module (R M : Type*) [Semiring R] [AddCommMonoid M]
-- In a context with `S A : Type` and instances `[CommSemiring S] [Semiring A]`:
reifyKey? `Module #[.bvar 0, .bvar 1] #[S, A] = some ‹@Module S A inst₁ inst₂›
-- (`inst₁` and `inst₂` are synthesized by `mkClassApp?`.)

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.withGenericClassApp {α : Type} (name : Lean.Name) (k : Lean.Expr → Lean.Expr → Lean.MetaM (Option α)) : Lean.MetaM (Option α)

Run the continuation k on the "generic" application name.{…} a₁ … aₙ of n-ary class name on fresh local hypotheses a₁, …, aₙ plus the WHNF-reduced body of name's signature (which corresponds to the signature's conclusion only if said conclusion has no leading ∀-expressions that forallTelescopeReducing would peel off).

Returns none without ever running k if name isn't in the environment, or if the generic application isn't a class application.

For motivation, see isSubsingletonClass.

---

Examples

withGenericClassApp `Small k = k ‹@Small.{?w, ?v} α› ‹Prop›
withGenericClassApp `Module k = k ‹@Module.{?u, ?v} R M inst₁ inst₂› ‹Type (max ?u ?v)›
withGenericClassApp `Nat.succ k = none

Equations

• One or more equations did not get rendered due to their size.