Derive generators on inductives with struct params

[mwhicks1]

Support structure-parameterized output types in the constrained deriver derive_generator/derive_mutual could not produce values of an inductive parameterized by a structure (e.g. Strata's LExpr T where T : LExprParams carries the metadata/identifier/type-annotation types). The structure parameter T.mono : LExprParamsT rides along as an argument of every constructor, and the deriver tried to generate it — yielding a Type 1-in-Type universe error — and had no way to generate the per-constructor metadata fields (m : T.base.Metadata). This mirrors the gap that Specimen.DeriveArbitrary fixes for the unconstrained deriving Arbitrary path via expandStructBinders.

Three coordinated changes make the fully-parameterized relation derivable:

1. Don't lift fixed, ungeneratable subterms during conclusion flattening (Utils.lean). collectUnmatchableSubterms now skips a subterm whose free variables are all fixed inputs and whose type has no Arbitrary instance (e.g. T.mono). Ordinary fixed value subterms like n * n : Nat still flatten (they have Arbitrary), so checker behavior is unchanged. The fixed-input set is the conclusion's non-output bare-variable arguments (DeriveConstrainedProducer).

2. Emit per-field producer instance binders for structure parameters (MakeConstrainedProducerInstance.lean). New expandStructInstBinders / mkProducerParamInstBinders mirror expandStructBinders: a sort param α keeps [Arbitrary α] [DecidableEq α]; a structure param T expands to [Arbitrary T.base.Metadata] … . Threaded through both the single-instance and mutual-def emission paths (the latter places struct-field binders innermost, where the value param they reference is in scope).

3. Drop implicit constructor arguments from conclusion outputs (MExp.lean). dropImplicitCtorArgsExpr removes implicit-position args of each data constructor in the produced value (e.g. LExpr.const's T, Option.some's α) so the implicit-allowing emission re-infers them instead of mis-placing them positionally.

StrataLexprGen now derives a generator for the genuine @LExpr.HasTypeA T … (abstract T, no monomorphization) and its embedded #eval confirms soundness: 60/60 sampled terms type-check, using the LExpr typechecking algorithm, at the requested type. Full test suite green.

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

[ngernest]

Here, we call mkConst without specifying universe levels -- this is fine for Strata in practice since the parameterized types are all Type 0. However, in the future, if we have types parameterized by universe-polymorphic structures (see example below), the projType would be computed incorrectly. To fix this, we would need to extract the universe levels from ty (the type expression for the structure) and pass them to mkConst. I don't think universe-polymorphic structures are that common in practice, so it's fine to leave it out, but wanted to bring this up just in case.

Here's an example of a universe-polymorphic structure parameter:

-- Universe-polymorphic structure type
structure Config.{v} where
    Carrier : Type v
    default : Carrier

-- Config.{0} gives Carrier : Type 0, Config.{1} gives Carrier : Type 1
inductive Tree (C : Config.{u}) : Type u where
    | leaf : C.Carrier → Tree C
    | node : Tree C → Tree C → Tree C

[mwhicks1]

Rather than try to address this, I left a "Limitation" comment that documents the weakness.

[ngernest]

Looks good, thanks!

[ngernest]

Looks generally good to me! Left a few minor comments

[ngernest]

Looks great, thanks!

The base branch was changed.

[segevem]

One of my PRs modifies the way we track bracketed typeclass instance arguments to only collect those that are truly necessary. It does so by traversing the dependency graph and propagating bottom up the needed dependencies from the schedules. My only concern is how well this change would adapt to that.

[mwhicks1]

Canceling this in favor of PR #47