doc: update inferInstanceAs docstring and rename normalizeInstance to wrapInstance (#13115)

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>

src/Init/Prelude.lean

@@ -185,15 +185,21 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
-"instance normal form": the result is a constructor application whose sub-instance fields
-are canonical instances and whose types match `α` exactly. This is useful when `α` is
-definitionally equal to some `α'` for which instances are registered, as it prevents
-leaking the definition's RHS at lower transparencies. See `Lean.Meta.InstanceNormalForm`
-for details. Example:
+/-- `inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
+definitionally equal type if necessary. This is useful when `α` is definitionally equal to
+some `α'` for which instances are registered, as it prevents leaking the definition's RHS
+at lower transparencies.
+
+`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
+instance without transporting between types, use `inferInstance` instead.
+
+Example:
 ```
-#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
+def D := Nat
+instance : Inhabited D := inferInstanceAs (Inhabited Nat)
 ```
+
+See `Lean.Meta.WrapInstance` for details.
 -/
 abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
 

src/Lean/Elab/BuiltinTerm.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Meta.Diagnostics
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Elab.Open
 public import Lean.Elab.SetOption
 public import Lean.Elab.Eval
@@ -334,10 +334,10 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let type ← abstractInstImplicitArgs type
   let inst ← synthInstance type
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
-    -- Normalize to instance normal form.
+    -- Wrap instance so its type matches the expected type exactly.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
     let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
+    withNewMCtxDepth <| wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Deriving/Basic.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.Elab.App
 public import Lean.Elab.DeclNameGen
 import Lean.Compiler.NoncomputableAttr
-import Lean.Meta.InstanceNormalForm
+import Lean.Meta.WrapInstance
 
 public section
 
@@ -211,10 +211,10 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
           -- We don't reduce because of abbreviations such as `DecidableEq`
           forallTelescope classExpr fun _ classExpr => do
             let result ← mkInst classExpr declName decl value
-            -- Save the pre-normalization value for the noncomputable check below,
-            -- since `normalizeInstance` may inline noncomputable constants.
+            -- Save the pre-wrapping value for the noncomputable check below,
+            -- since `wrapInstance` may inline noncomputable constants.
             let preNormClosure ← Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
-            -- Compute instance name early so `normalizeInstance` can use it for aux def naming.
+            -- Compute instance name early so `wrapInstance` can use it for aux def naming.
             let env ← getEnv
             let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" preNormClosure.type)
             instName ← liftMacroM <| mkUnusedBaseName instName
@@ -223,7 +223,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
-                normalizeInstance result.instVal result.instType
+                wrapInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
                   (isMeta := isMeta)
             else

src/Lean/Elab/PreDefinition/Basic.lean

@@ -10,7 +10,7 @@ public import Lean.Compiler.NoncomputableAttr
 public import Lean.Util.NumApps
 public import Lean.Meta.Eqns
 public import Lean.Elab.RecAppSyntax
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Elab.DefView
 public section
 

src/Lean/Meta.lean

@@ -27,7 +27,7 @@ public import Lean.Meta.Match
 public import Lean.Meta.ReduceEval
 public import Lean.Meta.Closure
 public import Lean.Meta.AbstractNestedProofs
-public import Lean.Meta.InstanceNormalForm
+public import Lean.Meta.WrapInstance
 public import Lean.Meta.LetToHave
 public import Lean.Meta.ForEachExpr
 public import Lean.Meta.Transform

src/Lean/Meta/WrapInstance.lean

@@ -13,17 +13,16 @@ public import Lean.Meta.CtorRecognizer
 public section
 
 /-!
-# Instance Normal Form
+# Instance Wrapping
 
-Both `inferInstanceAs` and the default `deriving` handler normalize instance bodies to
-"instance normal form". This ensures that when deriving or inferring an instance for a
-semireducible type definition, the definition's RHS is not leaked when reduced at lower
-than semireducible transparency.
+Both `inferInstanceAs` and the default `deriving` handler wrap instance bodies to ensure
+that when deriving or inferring an instance for a semireducible type definition, the
+definition's RHS is not leaked when reduced at lower than semireducible transparency.
 
 ## Algorithm
 
 Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
-`normalizeInstance` constructs a result instance as follows, executing all steps at
+`wrapInstance` constructs a result instance as follows, executing all steps at
 `instances` transparency:
 
 1. If `I'` is not a class, return `i` unchanged.
@@ -46,7 +45,7 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 
 ## Options
 
-- `backward.inferInstanceAs.wrap`: master switch for normalization in both `inferInstanceAs`
+- `backward.inferInstanceAs.wrap`: master switch for wrapping in both `inferInstanceAs`
   and the default `deriving` handler
 - `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for sub-instance
   fields to avoid non-defeq instance diamonds
@@ -59,7 +58,7 @@ namespace Lean.Meta
 
 register_builtin_option backward.inferInstanceAs.wrap : Bool := {
   defValue := true
-  descr := "normalize instance bodies to constructor-based normal form in `inferInstanceAs` and the default `deriving` handler"
+  descr := "wrap instance bodies in `inferInstanceAs` and the default `deriving` handler"
 }
 
 register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
@@ -77,7 +76,7 @@ register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
   descr := "wrap data fields in auxiliary definitions to fix their types"
 }
 
-builtin_initialize registerTraceClass `Meta.instanceNormalForm
+builtin_initialize registerTraceClass `Meta.wrapInstance
 
 /--
 Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
@@ -95,16 +94,16 @@ def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   instantiateMVars (mkAppN fn args)
 
 /--
-Normalize an instance value to "instance normal form".
+Wrap an instance value so its type matches the expected type exactly.
 See the module docstring for the full algorithm specification.
 -/
-partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
+partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
     (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
-  withTraceNode `Meta.instanceNormalForm
+  withTraceNode `Meta.wrapInstance
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
     | return inst
-  trace[Meta.instanceNormalForm] "class is {className}"
+  trace[Meta.wrapInstance] "class is {className}"
 
   if ← isProp expectedType then
     if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
@@ -117,7 +116,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
   inst.withApp fun f args => do
     let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo
       | do
-        trace[Meta.instanceNormalForm] "did not reduce to constructor application, returning/wrapping as is: {inst}"
+        trace[Meta.wrapInstance] "did not reduce to constructor application, returning/wrapping as is: {inst}"
         if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
           let instType ← inferType inst
           if ← isDefEq expectedType instType then
@@ -135,11 +134,11 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
           return inst
     let (mvars, _, cls) ← forallMetaTelescope (← inferType f)
     if h₁ : args.size ≠ mvars.size then
-      throwError "instance normal form: incorrect number of arguments for \
+      throwError "wrapInstance: incorrect number of arguments for \
         constructor application `{f}`: {args}"
     else
       unless ← isDefEq expectedType cls do
-        throwError "instance normal form: `{expectedType}` does not unify with the conclusion of \
+        throwError "wrapInstance: `{expectedType}` does not unify with the conclusion of \
           `{.ofConstName ci.name}`"
       for h₂ : i in ci.numParams...args.size do
         have : i < mvars.size := by
@@ -155,7 +154,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
           if ← isDefEq argExpectedType argType then
             mvarId.assign arg
           else
-            trace[Meta.instanceNormalForm] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
+            trace[Meta.wrapInstance] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
             mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
         -- Recurse into instance arguments of the constructor
         else if (← isClass? argExpectedType).isSome then
@@ -165,12 +164,12 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             -- semireducible transparency.
             try
               if let .some new ← trySynthInstance argExpectedType then
-                trace[Meta.instanceNormalForm] "using existing instance {new}"
+                trace[Meta.wrapInstance] "using existing instance {new}"
                 mvarId.assign new
                 continue
             catch _ => pure ()
 
-          mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
+          mvarId.assign (← wrapInstance arg argExpectedType (compile := compile)
             (logCompileErrors := logCompileErrors) (isMeta := isMeta))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.

src/Lean/Parser/Term.lean

@@ -774,10 +774,15 @@ In particular, it is like a unary operation with a fixed parameter `b`, where on
 @[builtin_term_parser] def noImplicitLambda := leading_parser
   "no_implicit_lambda% " >> termParser maxPrec
 /--
-`inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
-"instance normal form": the result is a constructor application whose sub-instance
-fields are canonical instances and whose types match `α` exactly. See
-`Lean.Meta.InstanceNormalForm` for details.
+`inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
+definitionally equal type if necessary. This is useful when `α` is definitionally equal to
+some `α'` for which instances are registered, as it prevents leaking the definition's RHS
+at lower transparencies.
+
+`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
+instance without transporting between types, use `inferInstance` instead.
+
+See `Lean.Meta.WrapInstance` for details.
 -/
 @[builtin_term_parser] def «inferInstanceAs» := leading_parser
   "inferInstanceAs" >> (((" $ " <|> " <| ") >> termParser minPrec) <|> (ppSpace >> termParser argPrec))

tests/elab/12897.lean

@@ -1,4 +1,4 @@
--- Tests that `normalizeInstance` auxiliary definitions work correctly
+-- Tests that `wrapInstance` auxiliary definitions work correctly
 -- when used inside a `meta` section, for both `inferInstanceAs` and `deriving`.
 
 module
@@ -11,7 +11,7 @@ namespace Test
 
 open Lean
 
--- `@[expose]` forces `normalizeInstance` to create aux wrapper definitions,
+-- `@[expose]` forces `wrapInstance` to create aux wrapper definitions,
 -- which is where the meta marking matters.
 @[expose] def Foo := Unit
 deriving Inhabited

tests/elab/Reparen.lean.out.expected

@@ -185,15 +185,21 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
-"instance normal form": the result is a constructor application whose sub-instance fields
-are canonical instances and whose types match `α` exactly. This is useful when `α` is
-definitionally equal to some `α'` for which instances are registered, as it prevents
-leaking the definition's RHS at lower transparencies. See `Lean.Meta.InstanceNormalForm`
-for details. Example:
+/-- `inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
+definitionally equal type if necessary. This is useful when `α` is definitionally equal to
+some `α'` for which instances are registered, as it prevents leaking the definition's RHS
+at lower transparencies.
+
+`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
+instance without transporting between types, use `inferInstance` instead.
+
+Example:
 ```
-#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
+def D := Nat
+instance : Inhabited D := inferInstanceAs (Inhabited Nat)
 ```
+
+See `Lean.Meta.WrapInstance` for details.
 -/
 abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i