This PR updates the `inferInstanceAs` docstring to reflect current
behavior: it requires an
expected type from context and should not be used as a simple
`inferInstance` synonym. The
old example (`#check inferInstanceAs (Inhabited Nat)`) no longer works,
so it's replaced
with one demonstrating the intended transport use case.
Additionally, renames `InstanceNormalForm.lean` to `WrapInstance.lean`,
`normalizeInstance`
to `wrapInstance`, and the trace class `Meta.instanceNormalForm` to
`Meta.wrapInstance`,
removing the "instance normal form" terminology from both documentation
and code.
Context:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/inferInstanceAs.20is.20broken/near/581449313🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR switches `normalizeInstance` from using `isMetaSection` to the
existing `declName?` pattern (already used by `unsafe` in
`BuiltinNotation.lean` and `private_decl%` in `BuiltinTerm.lean`) for
determining whether aux defs should be marked `meta`.
#13043 used `isMetaSection` to determine whether `normalizeInstance` aux
defs should be marked `meta`. This caused `deriving` in meta sections to
fail: the deriving handler doesn't mark the instance itself as meta, so
the non-meta instance couldn't access its meta-marked aux defs:
```
Invalid definition `instInhabitedLibraryNote`, may not access declaration
`instInhabitedLibraryNote._aux_1` marked as `meta`
```
The `declName?` pattern inherits meta status from the parent declaration
rather than the scope. This correctly handles both cases:
- **`inferInstanceAs`**: parent declaration is marked meta by
`processHeaders`, so `declName?.any (isMarkedMeta env)` is true and aux
defs are correctly marked meta
- **`deriving`**: `declName?` is `none` (the deriving handler runs
outside `withDeclName`), so `isMeta` is `false` and aux defs are not
marked meta — matching the instance itself, which the deriving handler
also does not mark meta
Found while adapting Batteries to nightly-2026-03-23.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR fixes a bug where `inferInstanceAs` and the default `deriving`
handler, when used inside a `meta section`, would create auxiliary
definitions (via `normalizeInstance`) that were not marked as `meta`.
This caused the compiler to reject the parent `meta` definition with:
```
Invalid `meta` definition `instEmptyCollectionNamePrefixRel`, `instEmptyCollectionNamePrefixRel._aux_1` not marked `meta`
```
The fix adds an `isMeta` parameter to `normalizeInstance` that is
propagated from the elaboration context (`isMarkedMeta` for
`inferInstanceAs`, `Scope.isMeta` for the deriving handler), and marks
each auxiliary definition created by `mkAuxDefinition` as `meta` when
appropriate.
Found while adapting Mathlib to
https://github.com/leanprover/lean4/pull/12897.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
