feat: improve error when an identifier is unbound because autoImplicit is off (#11119)

This PR introduces a clarifying note to "undefined identifier" error
messages when the undefined identifier is in a syntactic position where
autobinding might generally apply, but where and autobinding is
disabled. A corresponding note is made in the `lean.unknownIdentifier`
error explanation.

The core intended audience for this error message change is "newcomer
who would otherwise be baffled why the thing that works in this Mathlib
project gets 'unknown identifier' errors in this non-Mathlib project."

## Modified behavior

### Example 1
```lean4
set_option autoImplicit true in
set_option relaxedAutoImplicit false in
def thisBreaks (x : α₂) (y : size₂) := ()
```

Before:
```
Unknown identifier `size₂`
```

After:
```
Unknown identifier `size₂`

Note: It is not possible to treat `size₂` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
```

### Example 2
```lean4
set_option autoImplicit false in
def thisAlsoBreaks (x : α₃) (y : size₃) := ()
```

Before:
```
Unknown identifier `α₃`
Unknown identifier `size₃`
```

After:
```
Unknown identifier `α₃`

Note: It is not possible to treat `α₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
Unknown identifier `size₃`

Note: It is not possible to treat `size₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
```

## How this works

The elaboration process knows whether it is considering syntax where we
be able to auto-bind implicits thanks to information in the
`Lean.Elab.Term.Context`.

Before this PR, this contains:
* `autoBoundImplicit`, a boolean that is true when we are considering
syntax that might be able to auto-bind implicit AND when the
`autoImplicit` flag is set to true
* `autoBoundImplicits`, an array of `Expr` variables that we've
autobound

After this PR, this contains:
* `autoBoundImplicitCtx`, an option which is `some` **whenever** we are
considering syntax that might be able to auto-bind implicit, and carries
the array of exprs as well as a copy of the `autoImplicit` flag's value.
(The latter lets us re-implement the `autoBoundImplicit` flag for
backward compatibility.)

Therefore, rather than having access to "elaboration is in an
autobinding context && flag is enabled", it's possible to recover both
of those individual values, and give different information to the user
in cases where we didn't attempt autobinding but would have if different
options had been set.

## Rationale

The revised error message avoids offering much guidance — it doesn't
actively suggest setting the option to a different value or suggest
adding an implicit binding. Care needs to be taken here to make sure
advice is not misleading; as the accepted RFC in #6462 points out, a
substantial portion of autobinding failures are just going to be
misspellings.

I considered and then rejected a code action here to that would add a
local `set_option autoImplicit true`. This seems undesirable or
counterproductive — if a project like Mathlib has proactively disabled
`autoImplicit`, its odd to be pushing local exceptions.

A hint prompting the user to add an implicit binding would be more
proper, but only in certain circumstances — we want to be conservative
in suggesting specific code actions! In a situation like this one, we'd
want to _avoid_ giving the suggestion of adding a `{HasArr}` binding,
which I think either requires tricky heuristics or means we'd want the
elaboration to play through the consequences of auto-binding and make
sure it doesn't cause any follow-on errors before suggesting adding an
implicit binding.

```
set_option autoImplicit true
set_option relaxedAutoImplicit false
instance has_arr : HasArr Preorder := { Arr := Function }
```

Additionally, it seems like it would make the most sense to offer to
auto-bind _all_ the relevant unknown identifiers at once. To avoid being
misleading, this too would seem to require playing through the
consequences of autobinding before being able to safely suggest the
change. This is enough additional complexity that I'm leaving it for
future work.

---------

Co-authored-by: David Thrane Christiansen <[email protected]>

Author: robsimmons

src/Lean/Elab/AutoBound.lean

@@ -7,6 +7,8 @@ module
 
 prelude
 public import Lean.Data.Options
+public import Lean.Message
+public import Lean.Meta.Hint
 
 public section
 
@@ -24,7 +26,14 @@ register_builtin_option relaxedAutoImplicit : Bool := {
     descr    := "When \"relaxed\" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see option `autoImplicit`)."
   }
 
+/--
+Checks whether a string is a name that can be auto-bound when the `relaxedAutoImplicit` option is
+set to `false`.
 
+In "strict" auto implicit mode, a identifier can only be auto-bound if it is a single character (`α`
+or `x`) or has an arbitrary postfix sequence of numbers, subscripts, and underscores. Therefore,
+both `αᵣₒₛₑ₂₁₁'''` and `X123_45` can be auto-bound even with `relaxedAutoBound` set to `false`.
+-/
 private def isValidAutoBoundSuffix (s : String) : Bool :=
   s.toRawSubstring.drop 1 |>.all fun c => c.isDigit || isSubScriptAlnum c || c == '_' || c == '\''
 
@@ -39,17 +48,56 @@ Thus, in the example above, when `A` is expanded, a `x` with a fresh macro scope
 `x`+macros-scope is not in scope and is a valid auto-bound implicit name after macro scopes are erased.
 So, an auto-bound exception would be thrown, and `x`+macro-scope would be added as a new implicit.
 When, we try again, a `x` with a new macro scope is created and this process keeps repeating.
-Therefore, we do consider identifier with macro scopes anymore.
+Therefore, we don't consider identifier with macro scopes anymore.
+
+An `.error` value should be treated as a `false`—this is not a valid auto-bound implicit name—
+but it contains additional notes (above and beyond `Unknown identifier`) to attach to
+an error message.
 -/
 
-def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
+def checkValidAutoBoundImplicitName (n : Name) (allowed : Bool) (relaxed : Bool) : Except MessageData Bool :=
   match n with
-  | .str .anonymous s => s.length > 0 && (relaxed || isValidAutoBoundSuffix s)
-  | _ => false
+  | .str .anonymous s =>
+    if s.length = 0 then
+      .ok false
+    else if allowed && (relaxed || isValidAutoBoundSuffix s) then
+      .ok true
+    else if !allowed then
+      .error <| .note m!"It is not possible to treat `{.ofConstName n}` as an implicitly bound variable here because the `autoImplicit` option is set to `{.ofConstName ``false}`."
+    else
+      .error <| .note m!"It is not possible to treat `{.ofConstName n}` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `{.ofConstName ``false}`."
+  | _ => .ok false
 
 def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=
   match n with
   | .str .anonymous s => s.length > 0 && (relaxed || (s.front.isLower && isValidAutoBoundSuffix s))
   | _ => false
 
+/--
+Tracks extra context needed within the scope of `Lean.Elab.Term.withAutoBoundImplicit`
+-/
+public structure AutoBoundImplicitContext where
+  /--
+  This always matches the `autoImplicit` option; it is duplicated here in
+  order to support the behavior of the deprecated `Lean.Elab.Term.Context.autoImplicit`
+  method.
+  -/
+  autoImplicitEnabled : Bool
+  /--
+  Tracks a working set of variables that the auto-binding process currently
+  anticipates adding implicit binding for.
+  -/
+  boundVariables : PArray Expr := {}
+deriving Inhabited
+
+instance : EmptyCollection AutoBoundImplicitContext where
+  emptyCollection := AutoBoundImplicitContext.mk (autoImplicitEnabled := false) (boundVariables := {})
+
+/--
+Pushes a new variable onto the autoImplicit context, indicating that it needs
+to be bound as an implicit parameter.
+-/
+public def AutoBoundImplicitContext.push (ctx : AutoBoundImplicitContext) (x : Expr) :=
+  { ctx with boundVariables := ctx.boundVariables.push x }
+
 end Lean.Elab

src/Lean/Elab/Term/TermElabM.lean

@@ -258,33 +258,41 @@ structure Context where
   declName? : Option Name := none
   macroStack        : MacroStack      := []
   /--
-     When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
-     The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
-     the list of pending synthetic metavariables, and returns `?m`. -/
+  When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
+  The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
+  the list of pending synthetic metavariables, and returns `?m`.
+  -/
   mayPostpone : Bool := true
   /--
-     When `errToSorry` is set to true, the method `elabTerm` catches
-     exceptions and converts them into synthetic `sorry`s.
-     The implementation of choice nodes and overloaded symbols rely on the fact
-     that when `errToSorry` is set to false for an elaboration function `F`, then
-     `errToSorry` remains `false` for all elaboration functions invoked by `F`.
-     That is, it is safe to transition `errToSorry` from `true` to `false`, but
-     we must not set `errToSorry` to `true` when it is currently set to `false`. -/
+  When `errToSorry` is set to true, the method `elabTerm` catches
+  exceptions and converts them into synthetic `sorry`s.
+  The implementation of choice nodes and overloaded symbols rely on the fact
+  that when `errToSorry` is set to false for an elaboration function `F`, then
+  `errToSorry` remains `false` for all elaboration functions invoked by `F`.
+  That is, it is safe to transition `errToSorry` from `true` to `false`, but
+  we must not set `errToSorry` to `true` when it is currently set to `false`.
+  -/
   errToSorry : Bool := true
   /--
-     When `autoBoundImplicit` is set to true, instead of producing
-     an "unknown identifier" error for unbound variables, we generate an
-     internal exception. This exception is caught at `withAutoBoundImplicit`
-     which adds an implicit declaration for the unbound variable and tries again. -/
-  autoBoundImplicit  : Bool            := false
-  autoBoundImplicits : PArray Expr := {}
+  During elaboration we track the current context for adding auto-bound
+  implicit variables. (We mark the entry to such a region with
+  `withAutoBoundImplicit` and leave it with `withoutAutoBoundImplicit`.)
+
+  When the `autoImplicit` option is `false`, this context is only used to
+  affect error messages. When `autoImplicit` is `true` and an identifier is
+  unbound and potentially an auto-bound implicit, an internal exception is
+  thrown and caught at the closest surrounding `withAutoBoundImplicit`,
+  which adds an implicit declaration for the unbound variable and tries
+  again.
+  -/
+  autoBoundImplicitContext : Option AutoBoundImplicitContext := .none
   /--
-    A name `n` is only eligible to be an auto implicit name if `autoBoundImplicitForbidden n = false`.
-    We use this predicate to disallow `f` to be considered an auto implicit name in a definition such
-    as
-    ```
-    def f : f → Bool := fun _ => true
-    ```
+  A name `n` is only eligible to be an auto implicit name if `autoBoundImplicitForbidden n = false`.
+  We use this predicate to disallow `f` to be considered an auto implicit name in a definition such
+  as
+  ```
+  def f : f → Bool := fun _ => true
+  ```
   -/
   autoBoundImplicitForbidden : Name → Bool := fun _ => false
   /-- Map from user name to internal unique name -/
@@ -333,6 +341,12 @@ structure Context where
 abbrev TermElabM := ReaderT Context $ StateRefT State MetaM
 abbrev TermElab  := Syntax → Option Expr → TermElabM Expr
 
+@[deprecated "replace with a check of autoBoundImplicitContext" (since := "2025-11-11")]
+def Context.autoBoundImplicit (ctx : Context) : Bool :=
+  match ctx.autoBoundImplicitContext with
+    | .none => false
+    | .some subCtx => subCtx.autoImplicitEnabled
+
 abbrev FixedTermElab := Option Expr → TermElabM Expr
 
 unsafe def FixedTermElab.toFixedTermElabRefImpl (m : FixedTermElab) : FixedTermElabRef :=
@@ -635,7 +649,11 @@ instance : MonadParentDecl TermElabM where
   getParentDeclName? := getDeclName?
 
 instance : MonadAutoImplicits TermElabM where
-  getAutoImplicits := return (← read).autoBoundImplicits.toArray
+  getAutoImplicits := do
+    if let .some implicits := (← read).autoBoundImplicitContext then
+      pure implicits.boundVariables.toArray
+    else
+      pure #[]
 
 /--
 Executes `x` in the context of the given declaration name. Ensures that the info tree is set up
@@ -751,7 +769,11 @@ def liftLevelM (x : LevelElabM α) : TermElabM α := do
   let ctx ← read
   let mctx ← getMCtx
   let ngen ← getNGen
-  let lvlCtx : Level.Context := { options := (← getOptions), ref := (← getRef), autoBoundImplicit := ctx.autoBoundImplicit }
+  let lvlCtx : Level.Context := {
+    options := (← getOptions),
+    ref := (← getRef),
+    autoBoundImplicit := ctx.autoBoundImplicitContext.map (·.autoImplicitEnabled) |>.getD false
+  }
   match (x lvlCtx).run { ngen := ngen, mctx := mctx, levelNames := (← getLevelNames) } with
   | .ok a newS  => setMCtx newS.mctx; setNGen newS.ngen; setLevelNames newS.levelNames; pure a
   | .error ex _ => throw ex
@@ -1812,28 +1834,30 @@ def elabType (stx : Syntax) : TermElabM Expr := do
   Enable auto-bound implicits, and execute `k` while catching auto bound implicit exceptions. When an exception is caught,
   a new local declaration is created, registered, and `k` is tried to be executed again. -/
 partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
-  let flag := autoImplicit.get (← getOptions)
-  if flag then
-    withReader (fun ctx => { ctx with autoBoundImplicit := flag, autoBoundImplicits := {} }) do
-      let rec loop (s : SavedState) : TermElabM α := withIncRecDepth do
-        checkSystem "auto-implicit"
-        try
+  let autoImplicitEnabled := autoImplicit.get (← getOptions)
+  let initCtx : AutoBoundImplicitContext := { autoImplicitEnabled }
+  if autoImplicitEnabled then
+    let rec loop (s : SavedState) (ctx : AutoBoundImplicitContext) : TermElabM α := withIncRecDepth do
+      checkSystem "auto-implicit"
+      try
+        withReader ({ · with autoBoundImplicitContext := .some ctx }) <|
           withSaveAutoImplicitInfoContext k
-        catch
-          | ex => match isAutoBoundImplicitLocalException? ex with
-            | some n =>
-              -- Restore state, declare `n`, and try again
-              s.restore (restoreInfo := true)
-              withLocalDecl n .implicit (← mkFreshTypeMVar) fun x =>
-                withReader (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } ) do
-                  loop (← saveState)
-            | none   => throw ex
-      loop (← saveState)
+      catch
+        | ex => match isAutoBoundImplicitLocalException? ex with
+          | some n =>
+            -- Restore state, declare `n`, and try again
+            s.restore (restoreInfo := true)
+            withLocalDecl n .implicit (← mkFreshTypeMVar) fun x => do
+              loop (← saveState) (ctx.push x)
+          | none   => throw ex
+    loop (← saveState) initCtx
   else
-    k
+    -- Track whether we are in an auto-bound context regardless of whether
+    -- the `autoImplicit` flag is enabled; this can influence error messages.
+    withReader ({ · with autoBoundImplicitContext := .some initCtx}) k
 
 def withoutAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
-  withReader (fun ctx => { ctx with autoBoundImplicit := false, autoBoundImplicits := {} }) k
+  withReader (fun ctx => { ctx with autoBoundImplicitContext := .none }) k
 
 partial def withAutoBoundImplicitForbiddenPred (p : Name → Bool) (x : TermElabM α) : TermElabM α := do
   withReader (fun ctx => { ctx with autoBoundImplicitForbidden := fun n => p n || ctx.autoBoundImplicitForbidden n }) x
@@ -1922,7 +1946,7 @@ def addAutoBoundImplicitsInlayHint (autos : Array Expr) (inlayHintPos : String.P
   use-case may not be able to handle the metavariables in the array being given to `k`.
 -/
 def addAutoBoundImplicits (xs : Array Expr) (inlayHintPos? : Option String.Pos.Raw) : TermElabM (Array Expr) := do
-  let autos := (← read).autoBoundImplicits
+  let autos ← getAutoImplicits
   go autos.toList #[]
 where
   go (todo : List Expr) (autos : Array Expr) : TermElabM (Array Expr) := do
@@ -2034,10 +2058,14 @@ where
     if env.isExporting then
       if let [(npriv, _)] ← withoutExporting <| resolveGlobalName (enableLog := false) n then
         throwUnknownIdentifierAt (declHint := npriv) stx m!"Unknown identifier `{.ofConstName n}`"
-    if (← read).autoBoundImplicit &&
-          !(← read).autoBoundImplicitForbidden n &&
-          isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
-      throwAutoBoundImplicitLocal n
+    if !(← read).autoBoundImplicitForbidden n then
+      if (← read).autoBoundImplicitContext.isSome then
+        let allowed := autoImplicit.get (← getOptions)
+        let relaxed := relaxedAutoImplicit.get (← getOptions)
+        match checkValidAutoBoundImplicitName n (allowed := allowed) (relaxed := relaxed) with
+          | .ok true => throwAutoBoundImplicitLocal n
+          | .ok false => throwUnknownIdentifierAt (declHint := n) stx m!"Unknown identifier `{.ofConstName n}`"
+          | .error msg => throwUnknownIdentifierAt (declHint := n) stx (m!"Unknown identifier `{.ofConstName n}`" ++ msg)
     throwUnknownIdentifierAt (declHint := n) stx m!"Unknown identifier `{.ofConstName n}`"
 
 /--

src/Lean/ErrorExplanations/UnknownIdentifier.lean

@@ -184,6 +184,51 @@ the expected type of the expression in which it occurs, which—due to the type
 this code seemingly intended—use *generalized field notation* as shown in the first corrected
 example. Alternatively, the correct namespace can be explicitly specified by writing the fully
 qualified function name.
+
+## Auto-bound variables
+
+```lean broken
+set autoImplicit false in
+def thisBreaks (x : α₁) (y : size₁) := ()
+
+set relaxedAutoImplicit false in
+def thisBreaks (x : α₂) (y : size₂) := ()
+```
+```output
+Unknown identifier `size₁`
+
+Note: It is not possible to treat `size₁` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
+Unknown identifier `α₂`
+
+Note: It is not possible to treat `α₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
+Unknown identifier `size₂`
+
+Note: It is not possible to treat `size₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
+```
+```lean fixed (title := "Fixed (modifying options)")
+set autoImplicit true in
+def thisBreaks (x : α₁) (y : size₁) := ()
+
+set relaxedAutoImplicit true in
+def thisBreaks (x : α₂) (y : size₂) := ()
+```
+```lean fixed (title := "Fixed (add implicit bindings for the unknown identifiers)")
+set autoImplicit false in
+def thisBreaks {size₁} (x : α₁) (y : size₁) := ()
+
+set relaxedAutoImplicit false in
+def thisBreaks {α₂ size₂} (x : α₂) (y : size₂) := ()
+```
+
+Lean's default behavior, when it encounters an identifier it can't identify in the type of a
+definition, is to add [automatic implicit parameters](lean-manual://section/automatic-implicit-parameters)
+for those unknown identifiers. However, many files or projects disable this feature by setting the
+`autoImplicit` or `relaxedAutoImplicit` options to `false`.
+
+Without re-enabling the `autoImplicit` or `relaxedAutoImplicit` options, the easiest way to fix
+this error is to add the unknown identifiers as [ordinary implicit parameters](lean-manual://section/implicit-functions)
+as shown in the example above.
+
 -/
 register_error_explanation lean.unknownIdentifier {
   summary := "Failed to resolve identifier to variable or constant."

tests/lean/1011.lean.expected.out

@@ -1 +1,3 @@
 1011.lean:6:11-6:13: error(lean.unknownIdentifier): Unknown identifier `AA`
+
+Note: It is not possible to treat `AA` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.

tests/lean/autoBoundImplicits1.lean.expected.out

@@ -2,12 +2,26 @@ myid 10 : Nat
 myid true : Bool
 autoBoundImplicits1.lean:16:4-16:11: warning: declaration uses 'sorry'
 autoBoundImplicits1.lean:20:25-20:29: error(lean.unknownIdentifier): Unknown identifier `size`
+
+Note: It is not possible to treat `size` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
 autoBoundImplicits1.lean:24:23-24:24: error(lean.unknownIdentifier): Unknown identifier `α`
+
+Note: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
 autoBoundImplicits1.lean:24:25-24:26: error(lean.unknownIdentifier): Unknown identifier `n`
+
+Note: It is not possible to treat `n` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
 autoBoundImplicits1.lean:24:33-24:34: error(lean.unknownIdentifier): Unknown identifier `α`
+
+Note: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
 autoBoundImplicits1.lean:24:37-24:38: error(lean.unknownIdentifier): Unknown identifier `β`
+
+Note: It is not possible to treat `β` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
 autoBoundImplicits1.lean:24:46-24:47: error(lean.unknownIdentifier): Unknown identifier `β`
+
+Note: It is not possible to treat `β` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
 autoBoundImplicits1.lean:24:48-24:49: error(lean.unknownIdentifier): Unknown identifier `n`
+
+Note: It is not possible to treat `n` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
 f {α : Type} {n : Nat} (xs : Vec α n) : Vec α n
 f mkVec : Vec ?m 0
 f mkVec : Vec Nat 0

tests/lean/autoBoundImplicits3.lean

@@ -0,0 +1,17 @@
+
+set_option autoImplicit true in
+set_option relaxedAutoImplicit true in
+set_option linter.unusedVariables false in
+def thisWorks (x : α₁) (y : size₁) := ()
+
+set_option autoImplicit true in
+set_option relaxedAutoImplicit false in
+def thisBreaks (x : α₂) (y : size₂) := ()
+
+set_option autoImplicit false in
+set_option relaxedAutoImplicit true in
+def thisAlsoBreaks (x : α₃) (y : size₃) := ()
+
+set_option autoImplicit false in
+set_option relaxedAutoImplicit false in
+def thisDefinitelyBreaks (x : α₄) (y : size₄) := ()

tests/lean/autoBoundImplicits3.lean.expected.out

@@ -0,0 +1,15 @@
+autoBoundImplicits3.lean:9:29-9:34: error(lean.unknownIdentifier): Unknown identifier `size₂`
+
+Note: It is not possible to treat `size₂` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
+autoBoundImplicits3.lean:13:24-13:26: error(lean.unknownIdentifier): Unknown identifier `α₃`
+
+Note: It is not possible to treat `α₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
+autoBoundImplicits3.lean:13:33-13:38: error(lean.unknownIdentifier): Unknown identifier `size₃`
+
+Note: It is not possible to treat `size₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
+autoBoundImplicits3.lean:17:30-17:32: error(lean.unknownIdentifier): Unknown identifier `α₄`
+
+Note: It is not possible to treat `α₄` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
+autoBoundImplicits3.lean:17:39-17:44: error(lean.unknownIdentifier): Unknown identifier `size₄`
+
+Note: It is not possible to treat `size₄` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.