Generator drops top-level `universe` commands and `CoeFun` instances → generated workspace fails to build

[kim-em]

Two @[eval_problem] source modules build fine under lake build / validate-manifest / check-problem-build, but their generated comparator workspaces fail to build, because EvalTools.Generate's extraction does not preserve everything the extracted declarations depend on. Both were only caught by check-generated-builds (i.e. CI), not by the source-level checks — so the gap is easy to hit unknowingly.

Gap 1 — top-level universe commands are not carried into Challenge.lean

A source module with

universe v u
def IsTopos (E : Type u) [Category.{v} E] : Prop := …
@[eval_problem] theorem fundamental_topos_theory {E : Type u} [Category.{v} E] (hE : IsTopos E) (X : E) : IsTopos (Over X) := by sorry

generates a Challenge.lean containing the theorem but not the universe v u command, so it fails:

error: Challenge.lean:6:43: unknown universe level `u`
error: Challenge.lean:6:57: unknown universe level `v`

The source module compiles fine; only the generated workspace breaks.

Gap 2 — CoeFun (and likely other) instances are not preserved into ChallengeDeps

A module whose trusted helpers rely on a CoeFun instance, e.g.

structure VolumePreservingEquiv (d : ℕ) where toMeasurableEquiv : Torus d ≃ᵐ Torus d; …
instance instCoeFunVPE (d : ℕ) : CoeFun (VolumePreservingEquiv d) (fun _ => Torus d → Torus d) where coe T := T.toMeasurableEquiv
noncomputable def deltaDist (T S : VolumePreservingEquiv d) : ℝ≥0∞ := essSup (fun x => edist (T x) (S x)) volume

generates a ChallengeDeps.lean that fails because the coercion is not in scope:

… this term has type VolumePreservingEquiv d
Note: Expected a function because this term is being applied to the argument x
error: build failed (target ChallengeDeps)

Again the source module compiles fine.

Repro

Observed on two real problems (now worked around in the problem statements):

• fundamental_topos_theory (Gap 1) — workaround: use auto-bound {E : Type*} [Category E] with no top-level universe.
• lax_approximation (Gap 2) — workaround: write T.toMeasurableEquiv x instead of T x and drop the CoeFun instance.

Both workarounds were verified with lake exe lean-eval generate --problem <id> + check-generated-builds --problem <id>.

Suggested fixes (any one closes the gap)

1. Preserve universe declarations in the extracted Challenge.lean/ChallengeDeps.lean (emit the module's universe command, or per-declaration universe binders).
2. Include instance declarations (notably CoeFun/CoeSort/coercions) that the holes or trusted helpers depend on, when building ChallengeDeps. The dependency closure should follow instances, not just def/theorems referenced by name.
3. Fail fast: have validate-manifest / the @[eval_problem] attribute reject (or warn on) modules that use a top-level universe command or define CoeFun instances that the current extractor can't carry — so authors hit it at source-check time, not after a ~2h generated CI build.

(1)+(2) are the real fixes; (3) is a cheap guard until then.

🤖 Prepared with Claude Code