Support structure-parameterized output types in the constrained deriver

[mwhicks1]

Teach derive_generator / derive_mutual to produce values of an inductive relation whose output type is parameterized by a structure (rather than a plain Sort/type parameter), as in Strata's LExpr T / LExpr.HasTypeA. Three coordinated, strictly-additive changes:

1. Don't lift fixed, ungeneratable subterms during conclusion flattening. Utils.lean gains allFVarsFixed / isFixedUngenerable and threads a fixed set of input fvars through collectUnmatchable{,Proper}Subterms; a subterm determined entirely by fixed inputs whose type has no Arbitrary instance (e.g. a structure parameter projection T.mono) is left in place instead of lifted into a generated unknown. DeriveConstrainedProducer.lean adds the fixedFVars parameter to linearizeAndFlatten and computes it from the conclusion's non-output bare-fvar arguments.

2. Emit per-field producer-instance binders for structure parameters. MakeConstrainedProducerInstance.lean gains expandStructInstBinders (which recursively walks a structure-typed parameter, emitting [className proj] for each Type-valued leaf) and mkProducerParamInstBinders, threaded through both the single-instance and mutual-def emission paths (struct-field binders innermost in the latter) and all wrapper instance commands.

3. Drop implicit constructor arguments from conclusion outputs. MExp.lean gains dropImplicitCtorArgsExpr and makes scheduleToMExp monadic, so implicit args (e.g. an output type's structure parameter) are omitted and re-inferred by Lean rather than mis-placed positionally.

Also add the missing Enum Unit primitive instance alongside Enum Bool, and the generatableVars -> generableVars rename in SearchTree.lean.

Test: SpecimenTest/DeriveArbitrarySuchThat/DeriveStructParamGenerator.lean derives a generator and an enumerator together for a two-field (one nested) structure-parameterized STLC typing relation over the genuine abstract Tm P.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[ngernest]

Looks good to me! Left just two comments related to Lean metaprogramming

[ngernest]

I think this function could be optimized if we use some of the functions for manipulating Exprs from Lean's standard library:

def allFVarsFixed (fixed : Std.HashSet FVarId) (e : Expr) : Bool :=
    e.hasFVar && !e.hasAnyFVar (!fixed.contains ·)

where hasFVar and hasAnyFVar come from the stdlib.

Expr.hasAnyFVar : Expr -> (FVarId -> Bool) -> Bool short-circuits when it finds the first fvar that violates the user-supplied predicate, so it might be more efficient than calling collectFVarOccurrences (done in the current implementation), which has to construct an FVarIdMap (environment mapping FVarIds to their values) containing all the free variables in the Expr.

[ngernest]

It might be good to add a comment here explaining why we might have bvars.size ≠ argsArr.size (this occurs when the constructor is not fully applied to its arguments).

Also, there is an implicit invariant being maintained here that the T (the type paramater to the inductive relation that is also a structure) appears at index 0 of args if the constructor is fully applied to all its arguments, including its implicit ones, so dropping implicit constructor arguments via this function drops T. (Technically, this is already enforced by classifyAppArgs in Schedules.lean, but this seems like useful documentation to have here)

[ngernest]

Regarding the toolchain difference between Specimen and Strata (Specimen uses Lean 4.30 whereas Strata uses 4.29.1), I'm not sure if there is an easy way around this, beyond creating a branch on Specimen to use 4.29.1 specifically and have all the Strata imports on this branch (this is what is done with Basalt).

[segevem]

Sort-typed variables in structure parameters should get Arbitrary/Enum/DecidableEq constraints only when strictly needed, as per #42 . Currently, they are hardcoded and thus require more instances than strictly necessary and might not compose properly.

[segevem]

Add another example that shows that without the Enum alpha this fails to infer?

[segevem]

Suggested regression tests: struct-param leaf-binder discovery gaps

Reviewing the leaf-binder machinery against the plain type-variable path (computeSpecConstraints / synthExternalConstraints / propagateConstraints), the leaf path discovers strictly less: it pattern-matches a fixed catalogue of step kinds onto hardcoded classes, where the plain path synthesizes-and-reads-back. Below are two tests that isolate real gaps, each paired with a plain type-variable control of the identical shape.

What I verified vs. designed:

• Both plain-α controls were run against the pre-Support structure-parameterized output types in the constrained deriver #47 build and pass — including the sharp probe that Gap B's generator requires [MyHashable α] (fails synthesis without it, succeeds with it), which proves the plain path propagates a non-standard class. Single-entry derive_mutual also works.
• The struct-leaf derive_mutual cases are build-unverified — the leaf deriver only exists on this branch and I built against the base. They're constructed by direct analogy to the verified controls; please run them here.

Scope note (a non-gap, ruled out empirically): neither path propagates constraints across separate derive_mutual commands — a plain-α generator checking an externally-derived checker also fails to find its [Enum α]. So this is a shared limitation, not a leaf-path regression, and I dropped a test I'd first drafted around it. Every test below keeps producer + dependency in one block.

Headline

The fix for Gap B is the same one that fixes Gap A: replace the hardcoded-class rules + boolean synthesis probe in computeStructLeafBinders with a leaf-level read-back — synthesize the dependency's instance and read back its actual instance-implicit binder domains (exactly what synthExternalConstraints does for plain params) — so any class, standard or custom, is discovered from use rather than assumed.

Gap A — compound type demands a different standard class than the producer's own

The compound branch probes feasibility (all of Arbitrary/Enum/DecidableEq in scope) then attaches the hardcoded producer class. If generating a compound over a leaf actually needs a different standard class, the wrong binder is emitted.

Gap B — a NON-standard class on a leaf is not propagated

computeStructLeafBinders attaches only Arbitrary/Enum/DecidableEq, so a leaf handed to a dependency requiring a custom class (MyHashable) never gets [MyHashable P.A] emitted. This is the limitation named in the "Known limitations" section — and it is leaf-path-specific: verified that the plain-α analogue propagates the non-standard class correctly within a block.

Proposed fixture (SpecimenTest/DeriveArbitrarySuchThat/StructParamLeafConstraintGaps.lean):

import Specimen.DeriveConstrainedProducer
import Specimen.DeriveChecker
import Specimen.DeriveArbitrary
import Specimen.DeriveEnum
import Specimen.Enumerators
import Specimen.EnumeratorCombinators
import Specimen.ArbitrarySizedSuchThat
import Plausible.Arbitrary

/-! # Struct-param leaf-binder gaps vs. the plain type-variable path

`computeStructLeafBinders` / `propagateStructLeafBinders` are the leaf-granularity
analogue of the plain type-parameter machinery (`computeSpecConstraints` /
`synthExternalConstraints` / `propagateConstraints`), but discover strictly less.
Each test pairs a **struct-leaf case** (expected to fail on this branch) with a
**plain type-variable control** of the identical shape. The controls were verified
to PASS on the base branch, so a control passing while its struct-leaf sibling fails
pins the failure to the leaf path, not to the shape.

NOTE on scope: both paths propagate constraints only *within a single* `derive_mutual`
block — neither propagates across separate `derive_mutual` commands (confirmed: a
plain-α generator that checks an externally-derived checker also fails to find its
`[Enum α]`). So every test keeps producer and dependency in ONE block; the gaps are
about *what the leaf path discovers within a block*. -/

open Plausible

/-! ## Gap A — compound type demands a *different* standard class than the producer's own -/
namespace GapA_WrongStandardClass

-- `Arbitrary (Boxed α)` is provided VIA `[Enum α]`, never `[Arbitrary α]`.
structure Boxed (α : Type) where
  tag : Nat
instance {α : Type} [Enum α] : Plausible.Arbitrary (Boxed α) where
  arbitrary := pure ⟨0⟩

structure BConfig where
  B : Type
inductive HasBox (P : BConfig) : Boxed P.B → Prop where
  | mk : ∀ b, HasBox P b

-- `E` has `Enum` but deliberately NO `Arbitrary`.
inductive E | e0 | e1
instance : Enum E where enum := pureEnum E.e0
abbrev BC : BConfig := ⟨E⟩

-- [GAP]: emits `[Arbitrary P.B]` (producer's own class) instead of the real `[Enum P.B]`.
--   TODAY: fails — demands an unsatisfiable `Arbitrary E` at `BC` and leaves the body's
--   real need `Enum P.B` unbound.   AFTER fix: emits `[Enum P.B]`, derives.
set_option specimen.autoDeriveDeps true in
set_option specimen.multiOutput true in
#guard_msgs(drop info, drop warning) in
derive_mutual
  generator (fun P => ∃ b : Boxed P.B, HasBox P b)

example : ArbitrarySizedSuchThat (Boxed BC.B) (fun b => HasBox BC b) := inferInstance

-- ---- [CONTROL] plain `α` (VERIFIED passing on base branch) ----
inductive HasBoxα {α : Type} : Boxed α → Prop where
  | mk : ∀ b, HasBoxα (α := α) b

set_option specimen.autoDeriveDeps true in
set_option specimen.multiOutput true in
#guard_msgs(drop info, drop warning) in
derive_mutual
  generator (fun α => ∃ b : Boxed α, @HasBoxα α b)

example [Enum α] : ArbitrarySizedSuchThat (Boxed α) (fun b => @HasBoxα α b) := inferInstance

end GapA_WrongStandardClass

/-! ## Gap B — NON-standard class on a leaf is not propagated -/
namespace GapB_NonStandardClass

class MyHashable (α : Type) where
  myhash : α → Nat

structure HConfig where
  A : Type

inductive HashEq (P : HConfig) [MyHashable P.A] : P.A → Nat → Prop where
  | mk : ∀ (x : P.A), HashEq P x (MyHashable.myhash x)

-- Generating `∃ x, NotHashEq P x n` must CHECK `¬ HashEq P x n`, pulling in HashEq's
-- checker and hence its `[MyHashable P.A]` requirement.
inductive NotHashEq (P : HConfig) [MyHashable P.A] : P.A → Nat → Prop where
  | mk : ∀ (x : P.A) n, ¬ HashEq P x n → NotHashEq P x n

-- [GAP]: `[MyHashable P.A]` is never emitted (checker and generator).
--   TODAY: fails to derive.   AFTER fix (leaf-level read-back of the dependency's
--   actual instance-implicit binders, not a fixed class catalogue): derives.
set_option specimen.autoDeriveDeps true in
set_option specimen.multiOutput true in
#guard_msgs(drop info, drop warning) in
derive_mutual
  checker   (fun P [MyHashable P.A] (x : P.A) n => @HashEq P _ x n),
  generator (fun P [MyHashable P.A] (n : Nat) => ∃ x, @NotHashEq P _ x n)

instance : MyHashable Bool where myhash b := if b then 1 else 0
abbrev HC : HConfig := ⟨Bool⟩
example (n : Nat) : ArbitrarySizedSuchThat HC.A (fun x => @NotHashEq HC _ x n) := inferInstance

-- ---- [CONTROL] plain `α` (VERIFIED passing on base branch) ----
inductive HashEqα {α : Type} [MyHashable α] : α → Nat → Prop where
  | mk : ∀ (x : α), HashEqα x (MyHashable.myhash x)
inductive NotHashEqα {α : Type} [MyHashable α] : α → Nat → Prop where
  | mk : ∀ (x : α) n, ¬ HashEqα x n → NotHashEqα x n

set_option specimen.autoDeriveDeps true in
set_option specimen.multiOutput true in
#guard_msgs(drop info, drop warning) in
derive_mutual
  checker   (fun α [MyHashable α] (x : α) n => @HashEqα α _ x n),
  generator (fun α [MyHashable α] (n : Nat) => ∃ x, @NotHashEqα α _ x n)

-- Verified: synthesizes only WITH [MyHashable α] (non-standard class propagated into the
-- binder); FAILS without it — proving the plain path discovers it.
example [MyHashable α] [Arbitrary α] [DecidableEq α] (n : Nat) :
    ArbitrarySizedSuchThat α (fun x => @NotHashEqα α _ x n) := inferInstance

end GapB_NonStandardClass