The description-based `@[derive Param]` handler #

ParamDerive.lean specified the deriving-handler algorithm (its 6-step design note) and hand-ported the representative inductive shapes (R_sum/paramSum, R_nat/paramNat); ParamData.lean hand-ported R_prod/R_option/R_list. This file turns the front half of that spec into a running elaborator: an IndDesc extraction in AdapTT's style, a mixed-variance guard, and a generator that emits the relational lift R_<T> of a simple inductive uniformly from its constructor signatures — the constructor-wise Forall₂-shape congruence the hand-ports reproduce by hand.

Implemented vs. specified #

Running elaborator (this file, exercised by the demos below):

IndDesc / CtorDesc / FieldKind — AdapTT's IndDesc scheme: a constructor is a list of fields, each field classified as
- param i — a non-recursive covariant occurrence of the i-th type parameter (e.g. the a in Tree.leaf a),
- recursive — the inductive itself applied to the params (e.g. the subtrees in Tree.node),
- other — a parameter-free field type, lifted by equality.
Param.occPol — a polarity (variance) analysis of a parameter's occurrences in a field type, flipping polarity under each arrow domain.
Param.toIndDesc : Name → MetaM IndDesc — reads an InductiveVal via getConstInfoInduct, walks each constructor's field telescope (forallTelescopeReducing), and classifies every field. Here the mixed-variance guard applies: a parameter that occurs in both co- and contravariant position (the canonical non-example, e.g. a field of type A → A) is rejected with AdapTT's NonExample (Mixed variance); a purely contravariant occurrence is likewise rejected (a Param lift of A is a relation A → A' → Prop, which only supplies a covariant element relation).
Param.mkRelInductive : IndDesc → Name → CommandElabM (TSyntax \command)— the generator: emits `inductive R_<T> {A₀ A₀' …} (P₀ : A₀ → A₀' → Prop) … : T A₀ … → T A₀' … → Prop with one constructor per source constructor, each taking the per-field relatedness hypotheses (Pᵢ aⱼ aⱼ'for a param field; the recursiveR_<T> …for a recursive field;aⱼ = aⱼ'for anotherfield) and concluding `R_<T> P… (c a…) (c a'…). This is exactly the shape of R_sum/R_list` etc.
Param.mkParamMap1Cmds : IndDesc → Name → … — for a non-recursive inductive (records / enums — the crypto carriers), the relation is upgraded to a full annotated Param: it emits the forward map T.paramMap (constructor-wise, applying each parameter's forward map to the matching field) and the instance T.param_instance : Param .map3 .map0 (T A…) (T A'…) whose R is the generated R_<T>. The map_in_R and R_in_map proof fields are synthesized constructor-wise (cases + exact R_<T>.<c> … / simp [T.paramMap, …]) — a finite per-constructor term, no induction needed because no field is the inductive itself. Element inputs are taken at Param .map3 .map3 (the level supplying map/map_in_R/R_in_map, e.g. paramId's level). This is exactly the shape paramProd/paramOption reproduce by hand, at the forward-map3 level so the result feeds castViaParam.
Param.isUniformRecursive / Param.mkParamMapRecCmds — for a uniform-recursive inductive (List/Tree-shape: every recursive field is T applied to the same parameters), the same full Param .map3 .map0 instance is generated, but the three forward fields are recursive: T.paramMap by structural recursion (recurse on recursive fields), map_in_R by induction on the value, R_in_map by induction on the R_<T> derivation — recursive arms use the induction hypothesis, param arms the element Pⱼ.fwd.*. isUniformRecursive gates the path: non-uniform recursion (nesting / arrows / differing args / indices) stays relation-only.
Param.mkParamDeriveCmds / mkParamInstanceHandler — registered as the @[derive Param] deriving handler (registerDerivingHandler): on deriving instance Param for T (or a deriving Param clause) it elaborates the generated R_<T> relation and the T.paramMap / T.param_instance (non-recursive or uniform-recursive) into the environment.

What the map-instance synthesis covers, and the boundary:

Non-recursive inductives (records / enums): a full Param .map3 .map0 instance — forward map plus both graph inclusions — is synthesized generically (mkParamMap1Cmds, finite per-constructor terms). deriving Param on a crypto record yields a usable Param, not just R_<T>.
Uniform-recursive inductives (List/Tree-shape — every recursive field is the inductive applied to the same parameters): also a full Param .map3 .map0 instance (mkParamMapRecCmds). The forward map T.paramMap is generated by structural recursion (recurse on recursive fields; the equation compiler discharges termination); map_in_R by induction on the value (recursive arms use the IH, param arms Pⱼ.fwd.map_in_R); R_in_map by induction on the R_<T> derivation (recursive arms use the IH, param arms Pⱼ.fwd.R_in_map). This reproduces the hand-written paramList/paramOption of ParamData generically, at the full map3 forward level. The uniform-recursion guard is isUniformRecursive.
Non-uniform recursion is out of scope (the labelled residual): a recursive occurrence nested under another type former (List (T A)), applied to different arguments, under an arrow (higher-order recursion), or an indexed family. isUniformRecursive returns false, so the uniform map path does not apply. (For nested recursion the relation generator itself does not apply — its other-by-equality lift is ill-typed across the two parameter instantiations — and the registered handler declines iv.isNested inductives up front.)

So: the @[derive Param] attribute is registered and runs; both the non-recursive and the uniform-recursive path generate the relation and the forward map3 Param instance with the variance guard; non-uniform recursive map/proof synthesis is the labelled residual.

The description-based @[derive Param] handler #

Implemented vs. specified #

IndDesc: AdapTT's description of an inductive's constructor signatures #

Variance analysis and the mixed-variance guard #

The relation generator #

The Param .map3 instance generator (non-recursive inductives) #

The Param .map3 instance generator (uniform-recursive inductives) #

The Param .map3 instance generator (nested-List-recursive inductives) #

Registration as the @[derive Param] deriving handler #

Demos #

Recursive instance: Tree and MyList get the full map3 instance #

Nested-List recursive instance: RoseT gets the FULL map3 instance (Extension 1) #

Crypto-record demos: a derived Param .map3 .map0 instance in use #

The mixed-variance non-example is rejected #

The non-uniform-recursion boundary #

The description-based `@[derive Param]` handler #

`IndDesc`: AdapTT's description of an inductive's constructor signatures #

The `Param .map3` instance generator (non-recursive inductives) #

The `Param .map3` instance generator (uniform-recursive inductives) #

The `Param .map3` instance generator (nested-`List`-recursive inductives) #

Registration as the `@[derive Param]` deriving handler #

Recursive instance: `Tree` and `MyList` get the full `map3` instance #

Nested-`List` recursive instance: `RoseT` gets the FULL `map3` instance (Extension 1) #

Crypto-record demos: a derived `Param .map3 .map0` instance in use #