Level inference over Expr

The elaboration-time half of Transfer.Synthesis.ParamInfer: the same level inference, driven by a real Expr and the ambient @[param] registry rather than by the pure TyShape datatype.

It lives in its own module because a meta definition may not reference a plain declaration of its own module, while the pure half is consumed by compiled #guard and native_decide tests. Importing that half with public meta import makes it available here.

Walking real Lean Expr (the full-Expr front-end)

The TyShape API above acts on a simplified spine. This section provides the front-end: a MetaM walk over an actual Lean type Expr that produces a TyShape, which the existing genFrom/solve core then consumes unchanged. The walk:

• Expr.forallE _ dom body _ with body not depending on the bound variable (checked by Expr.hasLooseBVar body 0) ⇒ a non-dependent arrow node (arrowReq arithmetic). Both dom and body are recursed.
• Expr.forallE _ dom body _ whose body uses the bound variable ⇒ a dependent forallT node (forallReq arithmetic). The bound variable is instantiated with a fresh local (withLocalDecl) before recursing into the instantiated body, so loose bvars never escape into the recursion.
• a constant or an application whose head is a constant ⇒ a base leaf; its lower bound is the registry class of the head constant (see constLB).
• Sort/fvar/bvar/anything else ⇒ a base none leaf (minimum map0).

The class-bound resolver reflects the registry's information content: an RArrow PA PB c c' witness records that a constant transfers, not at which MapClass (no MapClass appears in RArrow). So a registered head gets the minimum nonzero level map1 (the paramOfMap : Param map1 map0 any transferable representation carries), and a caller may refine per-name via an explicit override map.

def Transfer.Param.constLB (override : Std.HashMap Lean.Name MapClass) (n : Lean.Name) : Lean.MetaM (Option MapClass)

The registry-driven lower bound for a head constant. Looks up override first (an explicit per-name class a caller can pin); otherwise, if the constant is in the ambient @[param] database (getParamDB), it carries at least map1 (the forward-map level paramOfMap provides for any transferable representation); otherwise no bound (none, i.e. the map0 minimum).

Equations

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

partial def Transfer.Param.exprToTyShape (override : Std.HashMap Lean.Name MapClass) : Lean.Expr → Lean.MetaM TyShape

Walk a real Lean type Expr into a TyShape (the full-Expr front-end). Non-dependent → ⇒ arrow; dependent Π ⇒ forallT (bound variable instantiated with a fresh fvar before recursing); constant/application head ⇒ base leaf with its registry lower bound; everything else ⇒ base none. The resulting TyShape is consumed by the unchanged genFrom/solve core.

def Transfer.Param.inferParamLevelsExpr (override : Std.HashMap Lean.Name MapClass) (e : Lean.Expr) : Lean.MetaM (Nat × Assign)

Infer the minimal MapClass per occurrence of a real type Expr. Walks the Expr into a TyShape (registry-driven leaf bounds), then reuses the pure inferParamLevels core. Returns (rootId, assignment).

Equations

• Transfer.Param.inferParamLevelsExpr override e = do let shape ← Transfer.Param.exprToTyShape override e pure (Transfer.Param.inferParamLevels shape)

def Transfer.Param.inferRootClassExpr (override : Std.HashMap Lean.Name MapClass) (e : Lean.Expr) : Lean.MetaM MapClass

Convenience: the minimal forward class at the root occurrence of a real type Expr. The Expr analogue of inferRootClass.

Equations

• Transfer.Param.inferRootClassExpr override e = do let __x ← Transfer.Param.inferParamLevelsExpr override e match __x with | (rootId, a) => pure (a.get rootId)

def Transfer.Param.inferParamLevelsConst (override : Std.HashMap Lean.Name MapClass) (declName : Lean.Name) : Lean.MetaM (Nat × Assign)

Infer minimal classes for a (possibly universe-polymorphic) declaration by name. Instantiates the declaration's universe parameters with fresh level metavariables, then walks the resulting type with inferParamLevelsExpr. This closes the "universe-polymorphic declarations are not walked" residual: the universe parameters are carried along (the polymorphic type binders are skipped by exprToTyShape), so the term-level arrow/Π structure infers exactly as it does for a monomorphic instance. The universe relation — relating Type u to Type v as objects — is the capped map4 level and is not inferred.

Equations

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

def Transfer.Param.inferRootClassConst (override : Std.HashMap Lean.Name MapClass) (declName : Lean.Name) : Lean.MetaM MapClass

The minimal forward class at the root of a (possibly universe-polymorphic) declaration's type. The by-name analogue of inferRootClassExpr.

Equations

• Transfer.Param.inferRootClassConst override declName = do let __x ← Transfer.Param.inferParamLevelsConst override declName match __x with | (rootId, a) => pure (a.get rootId)

Demos on real Lean type Exprs

Each run_meta block elaborates a Lean type via quotation, runs the Expr front-end, and logInfos the inferred root class; the output is pinned with #guard_msgs, so a regression fails the build. The first uses the empty override (no registry constants involved); the registered-constant demo pins a head via the override table so the registry-lower-bound path applies deterministically.

def Transfer.Param.elabTy (stx : Lean.TSyntax `term) : Lean.MetaM Lean.Expr

A type-elaboration helper: elaborate a term syntax to its Expr.

Equations

• Transfer.Param.elabTy stx = (do let e ← Lean.Elab.Term.elabTerm stx.raw none Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing Lean.instantiateMVars e).run'