Documentation

Transfer.Synthesis.ParamInfer

Variable-level minimal-class inference #

ParamSynth/ParamSynthExt synthesize Param witnesses at a fixed menu of levels; ParamResolve.param_resolve is a first | … macro with literally-written candidate levels. Neither infers the level: they require the target (m, n) up front and try a hardcoded list.

This module provides the constraint-graph minimal-class solver, the Lean analogue of upstream Trocq's level-inference pass (https://github.com/rocq-community/trocq, paper §4.4): "the [parametricity] class chosen must remain a variable until the end; a reduction algorithm determines the minimal acceptable class." Each Type-occurrence gets a class variable whose value is determined by least-fixpoint propagation over the MapClass lattice (ParamLevel.lean's proven le/meet), driven by the arrowReq/forallReq decision tables.

Design (explicit constraint graph, not Lean metavariables) #

The class of each occurrence is modeled as an explicit Nat-indexed variable with a current lower bound in the lattice, not a Lean metavariable:

map4 is never selected by minimization: it is the lattice top, so the least solution sits strictly below it whenever any solution exists — which is how inference stays off the proven-inconsistent univalent level (UnivalenceStatus).

Wiring (no change to param_resolve/HasParam) #

A level-directed resolver would call inferParamLevels on the (shape-abstracted) goal type, read off the minimal forward class m at the root occurrence, and then invoke the existing Param.weaken (by decide) … (inferInstance : HasParam …).param path at that m (the "synthesize-high, use-low" move ParamWeaken proves sound). This module exposes the function and documents the consumption point; it does not edit the resolver.

The full-Expr front-end (exprToTyShape/inferParamLevelsExpr) #

The TyShape core above is a simplified surface. The section "## Walking real Lean Expr" below closes that residual: exprToTyShape : Expr → MetaM TyShape walks an actual Lean type Expr — non-dependent → (an arrow node, arrowReq arithmetic), dependent Π (a forallT node, forallReq arithmetic, detected by Expr.hasLooseBVar on the body), and application/const heads (a base leaf whose lower bound comes from the @[param] registry via getParamDB). It then reuses the same genFrom/solve core — no new solver. inferParamLevelsExpr and inferRootClassExpr are the Expr analogues of inferParamLevels/inferRootClass.

Scope #

The Expr walk covers: non-dependent arrows, dependent Π (instantiating the bound variable with a fresh fvar), constant/application heads as leaves, and registry lower bounds (a @[param]-registered head constant lifts its leaf to map1, the level paramOfMap provides for any transferable representation; an explicit override table refines this per name). It does not cover: higher-order/operator spines beyond a const application head (the head is taken as the leaf; argument types are not re-walked), universe polymorphism (sort levels are ignored — every Sort/fvar/bvar is a map0 leaf), or term-level ⟦t⟧ translation (that is ParamTranslate). The registry path imposes only presence-driven bounds: the RArrow witnesses carry no machine-readable MapClass, so an exact per-witness class is taken from the optional override, defaulting to map1 on registry hit. The minimizer is a least-fixpoint solver over the proven lattice.

The simplified type shape (the constraint generator's input) #

source
inductive Transfer.Param.TyShape :
Type

A simplified type structure mirroring the dep_→/dep_Π cases of the real constraint generator. Each node optionally carries a user lower bound: a registered witness available only at class c forces that occurrence ≥ c. base is a leaf (an opaque type occurrence); arrow d c is d → c; forallT d c is the dependent ∀-spine (a : d) → c.

Instances For
    source
    def Transfer.Param.instReprTyShape.repr :
    TyShape → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Transfer.Param.instReprTyShape :
      Repr TyShape
      Equations
      source
      def Transfer.Param.TyShape.leaf :
      TyShape

      A base occurrence with no user lower bound (the common leaf).

      Equations
      Instances For

        Constraints over class variables #

        A class variable is a Nat id. A constraint is a lower bound demand on a variable: geq v c forces assignment v ≥ c directly; geqVar v w f forces assignment v ≥ f (assignment w) (a child-driven demand, where f is the relevant projection of an arrowReq/forallReq table entry). All constraints are monotone in the current assignment, which is what makes least-fixpoint propagation converge to the minimal solution.

        source
        inductive Transfer.Param.Constraint :
        Type

        A lower-bound constraint on class variables.

        Instances For

          The lattice as a join-semilattice for fixpoint propagation #

          The lattice gives meet (greatest lower bound). Least-fixpoint propagation raises variables, so it needs the join (least upper bound), derived from the proven le: join a b is the le-smaller of the two that is ≥ both, falling back up the chain. Since the only incomparable pair is map2a/map2b (both < map3), their join is map3.

          source
          def Transfer.Param.MapClass.join :
          MapClass → MapClass → MapClass

          The join (least upper bound) on MapClass. Total: the only incomparable pair {map2a, map2b} joins to map3 (their least common upper bound).

          Equations
          Instances For
            source
            theorem Transfer.Param.MapClass.le_join_left (a b : MapClass) :
            (fun (a b : MapClass) => a.le b = true) a (a.join b)

            The join is an upper bound (left).

            source
            theorem Transfer.Param.MapClass.le_join_right (a b : MapClass) :
            (fun (a b : MapClass) => a.le b = true) b (a.join b)

            The join is an upper bound (right).

            Constraint generation #

            genFrom n annotates TyShape with fresh variable ids ≥ n (a pre-order traversal: the node itself gets n, then its children), returning the root's id, the next free id, and the emitted constraints. For an arrow/forallT node, the emitted constraints implement the arrowReq/forallReq tables:

            A node's own user lower bound lb (on base) emits geq id c.

            source
            def Transfer.Param.arrowCodFwd (v : MapClass) :
            MapClass

            The codomain-forward requirement of arrowReq as a total function: at output forward class v, the codomain occurrence must carry this forward class (arrowReq v |>.2.2.1). Defaults to map0 only at the impossible none case, which arrowReq never returns.

            Equations
            Instances For
              source
              def Transfer.Param.arrowRootFromCod (c : MapClass) :
              MapClass

              The inverse of arrowCodFwd: the least arrow output class whose arrowReq codomain-forward slot covers a given codomain demand c (i.e. the smallest v with c ⊑ arrowCodFwd v). This is what turns a codomain's lower bound into the root's lower bound — the table read "backwards", exactly Trocq's per-combinator level arithmetic. Computed by scanning the lattice in ascending order and taking the first class that suffices. map4 is intentionally absent: no output class produces a map4 codomain slot (arrowReq map4 gives map3), so a map4 demand is unreachable and minimization stays below the top.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Transfer.Param.forallDom (v : MapClass) :
                MapClass

                The domain (backward) requirement of forallReq as a total function (map0 where the output is outside the univalence-free table — those outputs are never minimal). At output forward class v, the ∀-domain must carry backward class forallReq v.

                Equations
                Instances For
                  source
                  def Transfer.Param.forallRootFromDom (d : MapClass) :
                  MapClass

                  The inverse of forallDom: the least ∀ output class whose domain requirement covers a given domain demand d. Used to lift a domain's lower bound into the ∀-root's lower bound. Only {map0, map1} are univalence-free outputs, so anything beyond a map2a domain demand is outside the safe fragment and pins to map4 (never selected, since such a demand never arises in the univalence-free shapes).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Transfer.Param.genFrom :
                    Nat → TyShape → Nat × Nat × List Constraint

                    Generate fresh ids ≥ start and the constraint list for a TyShape. Returns (rootId, nextFree, constraints). Each arrow/forallT node emits two constraints linking its variable v to a child's: the downward table read (v drives the child's required class) and the upward inverse read (a child's lower bound drives v). The upward edge is what propagates a registered leaf bound to the root; the downward edge keeps children consistent once the root is fixed. Both are monotone, so the least fixpoint is the minimal consistent assignment.

                    Equations
                    Instances For
                      source
                      def Transfer.Param.TyShape.size :
                      TyShape → Nat

                      Total number of variables a shape allocates (its node count).

                      Equations
                      Instances For

                        The assignment and the fixpoint solver #

                        An assignment is a varId → MapClass map (defaulting unmentioned variables to map0, the minimum). One propagation pass raises each variable by the join of its current value and every constraint's demand. Iterating size-many passes reaches the least fixpoint: each pass can only raise values (monotone), the lattice has finite height ≤ 6, and there are size variables, so the chain stabilizes.

                        source
                        @[reducible, inline]
                        abbrev Transfer.Param.Assign :
                        Type

                        An assignment of classes to variable ids; missing ⇒ map0.

                        Equations
                        Instances For
                          source
                          def Transfer.Param.Assign.get (a : Assign) (v : Nat) :
                          MapClass

                          Read a variable's current class (default map0).

                          Equations
                          Instances For
                            source
                            def Transfer.Param.Constraint.demand (a : Assign) :
                            Constraint → Nat × MapClass

                            The demand a single constraint places on the current assignment: the class the target variable must be ≥.

                            Equations
                            Instances For
                              source
                              def Transfer.Param.stepOnce (cs : List Constraint) (a : Assign) :
                              Assign

                              One propagation pass: for every constraint, raise its target variable to the join of its current value and the constraint's demand.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def Transfer.Param.iterate (cs : List Constraint) :
                                Nat → Assign → Assign

                                Iterate stepOnce fuel times. With fuel ≥ size, this reaches the least fixpoint (finite-height lattice, monotone passes).

                                Equations
                                Instances For
                                  source
                                  def Transfer.Param.solve (nVars : Nat) (cs : List Constraint) :
                                  Assign

                                  The minimal-class solver. From a constraint list and a variable count, least-fixpoint-propagate from the all-map0 assignment. The result assigns each variable the least class satisfying every constraint. Fuel = nVars * 6 (variables × lattice height) guarantees the fixpoint is reached.

                                  Equations
                                  Instances For

                                    The entry point #

                                    source
                                    def Transfer.Param.inferParamLevels (t : TyShape) :
                                    Nat × Assign

                                    Infer the minimal MapClass per occurrence of a TyShape. Generates the constraint graph and least-fixpoint-solves it. Returns (rootId, assignment): assignment.get rootId is the minimal forward class the whole type requires; a level-directed resolver synthesizes at that class and Param.weakens down.

                                    Equations
                                    Instances For
                                      source
                                      def Transfer.Param.inferRootClass (t : TyShape) :
                                      MapClass

                                      Convenience: the minimal forward class at the root occurrence of a TyShape.

                                      Equations
                                      Instances For

                                        Demos #

                                        The three required scenarios. Each is a #guard (so it is checked at elaboration, failing the build if the solver regresses), plus an example recording the value.

                                        (a) Unconstrained arrow ⇒ map0 everywhere #

                                        source
                                        def Transfer.Param.demoUnconstrained :
                                        TyShape

                                        An unconstrained arrow base → base: no user lower bounds, so the root and both children minimize to map0 (the lattice bottom — nothing forces structure).

                                        Equations
                                        Instances For

                                          (b) Arrow whose codomain has a map3 lower bound ⇒ minimal class set by #

                                          arrowReq, not higher.

                                          The codomain occurrence is registered at class map3. The codomain-forward demand that propagates back to the root is arrowCodFwd (root); the least root class whose arrowReq codomain-forward slot is ≥ map3 is map3 itself (arrowReq map3 = (map0, map3, map3, map0)). So the root minimizes to exactly map3 — not map4.

                                          source
                                          def Transfer.Param.demoCodMap3 :
                                          TyShape

                                          base → base(map3): codomain forced to at least map3.

                                          Equations
                                          Instances For

                                            (c) Nested ∀/→ picks per-subterm minima (no global over-demand). #

                                            A forallT whose domain is unconstrained and whose codomain is an arrow with a map2a-registered codomain. The inner arrow's root must cover the map2a demand (minimal: map2a, since arrowReq map2a = (map0, map2b, map2a, map0)), while the outer ∀'s domain and the inner arrow's domain stay at map0 — demonstrating the solver minimizes per subterm rather than globally lifting everything.

                                            source
                                            def Transfer.Param.demoNested :
                                            TyShape

                                            ∀ (_ : base). (base → base(map2a)).

                                            Equations
                                            Instances For

                                              Monotone-correctness / termination notes (checked) #

                                              The solver is sound by construction on the lattice ParamLevel.lean proves: every stepOnce raises variables by join (so the assignment only increases, and stays the least that satisfies the constraints seen so far), and the iteration count nVars * 6 exceeds (variables × lattice height), so the fixpoint is reached. The demos above #guard the minimal values directly; the following records that one extra pass is a no-op at the fixpoint (idempotence), the operational face of "least fixpoint reached".