test: always give extra message when errors are in the scope of autobinding

src/Lean/Elab/App.lean

@@ -240,6 +240,11 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
         let validNames ← getFoundNamedArgs
         let fnName? := if f.isConst then some f.constName! else none
         throwInvalidNamedArg namedArg fnName? validNames
+/-
+      let ctx ← readThe Term.Context
+      withTraceNode `Elab (fun _ => pure m!"throwinerror {s.f} {ctx.autoBoundImplicitContext.map (·.boundVariables.toArray)}") do
+        logInfo m!"quirky {repr s.f}  {ctx.autoBoundImplicitContext.isSome}"
+-/
       -- Help users see if this is actually due to an indentation mismatch/other parsing mishaps:
       let extra := if let some (arg : Arg) := s.args[0]? then
         .note m!"Expected a function because this term is being applied to the argument\
@@ -1338,9 +1343,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
             fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which has no fields."
         let tupleHint ← mkTupleHint eType idx ref
         throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; \
-          {numFields.plural "the only valid index is 1" s!"it must be between 1 and {numFields}"}"
+          {plural numFields "the only valid index is 1" s!"it must be between 1 and {numFields}"}"
           ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \
-          {numFields} field{numFields.plural}"
+          {numFields} field{plural numFields}"
           ++ tupleHint
   | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do
     let env ← getEnv

src/Lean/Elab/ErrorUtils.lean

@@ -6,8 +6,9 @@ Authors: Rob Simmons
 module
 
 prelude
-import Init.Notation
-import Init.Data.String
+import Lean.Message
+
+namespace Lean
 
 /--
 Translate numbers (1, 2, 3, 212, 322 ...) to ordinals with appropriate English-language names for
@@ -35,31 +36,63 @@ def _root_.Nat.toOrdinal : Nat -> String
     else
       s!"{n}th"
 
+class HasOxfordStrings α where
+  emp : α
+  and : α
+  comma : α
+  commaAnd : α
+
+instance : HasOxfordStrings String where
+  emp := ""
+  and := " and "
+  comma := ", "
+  commaAnd := ", and "
+
+instance : HasOxfordStrings MessageData where
+  emp := ""
+  and := " and "
+  comma := ", "
+  commaAnd := ", and "
+
 /--
 Make an oxford-comma-separated list of strings.
 
  - `["eats"].toOxford == "eats"`
  - `["eats", "shoots"].toOxford == "eats and shoots"`
  - `["eats", "shoots", "leaves"] == "eats, shoots, and leaves"`
 -/
-def _root_.List.toOxford : List String -> String
-  | [] => ""
+def toOxford [Append α] [HasOxfordStrings α] : List α -> α
+  | [] => HasOxfordStrings.emp
   | [a] => a
-  | [a, b] => a ++ " and " ++ b
-  | [a, b, c] => a ++ ", " ++ b  ++ ", and " ++ c
-  | a :: as => a ++ ", " ++ toOxford as
+  | [a, b] => a ++ HasOxfordStrings.and ++ b
+  | [a, b, c] => a ++ HasOxfordStrings.comma ++ b  ++ HasOxfordStrings.commaAnd ++ c
+  | a :: as => a ++ HasOxfordStrings.comma ++ toOxford as
+
+class HasPluralDefaults α where
+  singular : α
+  plural : α → α
+
+instance : HasPluralDefaults String where
+  singular := ""
+  plural := (· ++ "s")
+
+instance : HasPluralDefaults MessageData where
+  singular := .nil
+  plural := (m!"{·}s")
 
 /--
 Give alternative forms of a string if the `count` is 1 or not.
 
- - `(1).plural == ""`
- - `(2).plural == "s"`
- - `(1).plural "wug" == "wug"`
- - `(2).plural "wug" == "wugs"`
- - `(1).plural "it" "they" == "it"`
- - `(2).plural "it" "they" == "they"`
+ - `(1) |> plural == ""`
+ - `(2) |> plural == "s"`
+ - `(1) |> plural "wug" == "wug"`
+ - `(2) |> plural "wug" == "wugs"`
+ - `(1) |> plural "it" "they" == "it"`
+ - `(2) |> plural "it" "they" == "they"`
 -/
-def _root_.Nat.plural (count : Nat) (singular : String := "") (plural : String := singular ++ "s") :=
+def plural [HasPluralDefaults α] (count : Nat)
+    (singular : α := HasPluralDefaults.singular)
+    (plural : α := HasPluralDefaults.plural singular) :=
   if count = 1 then
     singular
   else

src/Lean/Elab/MutualInductive.lean

@@ -614,6 +614,10 @@ private def collectUniverses (views : Array InductiveView) (r : Level) (rOffset
   let (_, acc) ← go |>.run {}
   if !acc.badLevels.isEmpty then
     withViewTypeRef views do
+      if indTypes.any (·.ctors.any (·.type.hasSyntheticSorry)) then
+        throwError "Type cannot be determined: some part of the definition contains an error"
+      if indTypes.any (·.ctors.any (·.type.hasSorry)) then
+        throwError "Type cannot be determined: some part of the definition contains `sorry`"
       let goodPart := Level.addOffset (Level.mkNaryMax acc.levels.toList) rOffset
       let badPart := Level.mkNaryMax (acc.badLevels.toList.map fun (u, k) => Level.max (Level.ofNat rOffset) (Level.addOffset u (rOffset - k)))
       let inferred := (Level.max goodPart badPart).normalize

src/Lean/Elab/SyntheticMVars.lean

@@ -262,17 +262,17 @@ def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option M
   -- Formulate error message
   let containMVars :=
     if simpleMVars then
-      nStuck.plural "is a metavariable" "are metavariables"
+      plural nStuck "is a metavariable" "are metavariables"
     else
-      nStuck.plural "contains metavariables" "contain metavariables"
+      plural nStuck "contains metavariables" "contain metavariables"
 
   let theTypeArguments :=
     if args.length = 1 then
       "the type argument"
     else
-      s!"the {(stuckArguments.toList.map (·.succ.toOrdinal)).toOxford} type {nStuck.plural "argument" "arguments"}"
+      s!"the {(stuckArguments.toList.map (·.succ.toOrdinal)) |> toOxford} type {plural nStuck "argument" "arguments"}"
 
-  return .some (.note m!"Lean will not try to resolve this typeclass instance problem because {theTypeArguments} to `{.ofConstName name}` {containMVars}. {nStuck.plural "This argument" "These arguments"} must be fully determined before Lean will try to resolve the typeclass."
+  return .some (.note m!"Lean will not try to resolve this typeclass instance problem because {theTypeArguments} to `{.ofConstName name}` {containMVars}. {plural nStuck "This argument" "These arguments"} must be fully determined before Lean will try to resolve the typeclass."
     ++ .hint' m!"Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `{MessageData.ofConstName ``Nat}`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.")
 
 /--

src/Lean/Elab/Term/TermElabM.lean

@@ -17,6 +17,7 @@ public import Lean.Elab.DeclarationRange
 public import Lean.Elab.WhereFinally
 public import Lean.Elab.InfoTree.InlayHints
 public meta import Lean.Parser.Term
+import all Lean.Elab.ErrorUtils
 
 
 
@@ -1276,7 +1277,28 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr :
   elaboration step with exception `ex`.
 -/
 def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do
-  logException ex
+  let autoBoundNames ←
+    (← readThe Term.Context).autoBoundImplicitContext
+      |>.map (·.boundVariables.toList)
+      |>.getD []
+      |>.mapM (·.fvarId!.getUserName)
+  if autoBoundNames.length > 0 then
+    if let .error ref msg := ex then
+      if msg.isTagged || msg.hasTag (· = `suppressAutoImplicitWarning) then
+        logException ex
+      else
+        let extra :=  m!"This error occurred after the identifier{plural autoBoundNames.length} \
+          {autoBoundNames.map (m!"`{.ofName ·}`") |> toOxford} had been identified as \
+          {plural autoBoundNames.length "a free variable" "free variables"} and automatically \
+          given {plural autoBoundNames.length "an implicit binding" "implicit bindings"}. \
+          {plural autoBoundNames.length m!"Is `{.ofName autoBoundNames[0]!}`" m!"Are those identifiers all"} \
+          supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to \
+          typos or missing `import` or `open` statements, and this may cause unexpected errors."
+        logException (.error ref (msg ++ .hint' extra))
+    else
+      logException ex
+  else
+    logException ex
   mkSyntheticSorryFor expectedType?
 
 /-- If `mayPostpone == true`, throw `Exception.postpone`. -/
@@ -1885,6 +1907,32 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
             withLocalDecl n .implicit (← mkFreshTypeMVar) fun x => do
               loop (← saveState) (ctx.push x)
           | none   => throw ex
+
+/-
+      withTraceNode `Elab (fun _ => pure m!"withabi {ctx.boundVariables.toList.length}") do
+      try
+        withReader ({ · with autoBoundImplicitContext := .some ctx }) <|
+          withSaveAutoImplicitInfoContext k
+      catch
+        | ex@(.internal id k) =>
+          if id == autoBoundImplicitExceptionId then
+            withTraceNode `Elab (fun _ => pure m!"catchInternal {k.getName `localId `x}") do
+            -- Restore state, declare a new temporary local variable, and try again
+            let n := k.getName `localId `x
+            s.restore (restoreInfo := true)
+            withLocalDecl n .implicit (← mkFreshTypeMVar) fun x => do
+              loop (← saveState) (ctx.push x)
+          else throw ex
+        | .error ref msg =>
+          withTraceNode `Elab (fun _ => pure m!"catchError {ref}") do
+            logInfo m!"ERROR AFTER BOUND: {ctx.autoImplicitEnabled} {ctx.boundVariables.toArray}"
+          throwErrorAt ref (msg ++ .hint' m!"warning {ref}")
+
+        | ex => match isAutoBoundImplicitLocalException? ex with
+          | some n =>
+          | none   => throw ex
+-/
+
     loop (← saveState) initCtx
   else
     -- Track whether we are in an auto-bound context regardless of whether

src/Lean/Message.lean

@@ -172,6 +172,15 @@ def kind : MessageData → Name
   | tagged n _              => n
   | _                       => .anonymous
 
+/--
+Check if the *outermost* constructor is `.tagged`.
+To check if a tag exists anywhere in the message, use `MessageData.hasTag (fun _ => true)`.
+-/
+def isTagged : MessageData → Bool
+  | .tagged .. => true
+  | _ => false
+
+
 def isTrace : MessageData → Bool
   | withContext _ msg       => msg.isTrace
   | withNamingContext _ msg => msg.isTrace

tests/lean/302.lean.expected.out

@@ -5,3 +5,5 @@ but this term has type
 
 Note: Expected a function because this term is being applied to the argument
   0
+
+Hint: This error occurred after the identifiers `m`, `a`, and `t` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.

tests/lean/3989_1.lean.expected.out

@@ -6,3 +6,5 @@ but this term has type
 
 Note: Expected a function because this term is being applied to the argument
   Expr
+
+Hint: This error occurred after the identifiers `Expr` and `MetaM` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.

tests/lean/3989_2.lean.expected.out

@@ -6,4 +6,6 @@ but this term has type
 
 Note: Expected a function because this term is being applied to the argument
   Expr
+
+Hint: This error occurred after the identifiers `Expr` and `MetaM` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.
 Nat : Type

tests/lean/autoBoundImplicits1.lean.expected.out

@@ -1,9 +1,11 @@
 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`
+autoBoundImplicits1.lean:20:25-20:29: error: 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`.
+
+Hint: This error occurred after the identifiers `α`, `β`, and `n` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.
 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`.

tests/lean/autoBoundImplicits3.lean.expected.out

@@ -1,6 +1,8 @@
-autoBoundImplicits3.lean:9:29-9:34: error(lean.unknownIdentifier): Unknown identifier `size₂`
+autoBoundImplicits3.lean:9:29-9:34: error: 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`.
+
+Hint: This error occurred after the identifier `α₂` had been identified as a free variable and automatically given an implicit binding. Is `α₂` supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.
 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`.

tests/lean/autoBoundPostponeLoop.lean.expected.out

@@ -3,3 +3,5 @@ autoBoundPostponeLoop.lean:5:12-5:18: error: invalid `▸` notation, argument
 has type
   ?m
 equality expected
+
+Hint: This error occurred after the identifiers `α`, `β`, and `h` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.

tests/lean/run/4920.lean

@@ -14,6 +14,8 @@ has type
   Vect m A
 but is expected to have type
   A
+
+Hint: This error occurred after the identifiers `A`, `m`, `i`, and `j` had been identified as free variables and automatically given implicit bindings. Are those identifiers all supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.
 ---
 error: Type mismatch: After simplification, term
   ih

tests/lean/univInference.lean

@@ -90,3 +90,15 @@ def ex7 (h : Stx = Nat) : True :=
   trivial
 
 end Induct
+
+inductive Sorry1 where
+  | x (a : Bool)
+  | y (b : sorry)
+
+inductive Sorry2 where
+  | x (a : Array Sorry2)
+  | y (b : sorry)
+
+inductive Sorry3 where
+  | x (a : Array Sorry3)
+  | y (b : x Err3)

tests/lean/univInference.lean.expected.out

@@ -31,3 +31,28 @@ univInference.lean:81:48-81:62: error: Invalid universe polymorphic resulting ty
   Sort (max u v)
 
 Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:98:0-100:17: error: Type cannot be determined: some part of the definition contains `sorry`
+univInference.lean:104:11-104:17: error: Function expected at
+  x
+but this term has type
+  ?m
+
+Note: Expected a function because this term is being applied to the argument
+  Err3
+
+Hint: This error occurred after the identifier `x` had been identified as a free variable and automatically given an implicit binding. Is `x` supposed to be implicitly bound? Automatic implicit binding can sometimes occur due to typos or missing `import` or `open` statements, and this may cause unexpected errors.
+univInference.lean:102:0-104:18: error: Type cannot be determined: some part of the definition contains an error

tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Lemmas.lean

@@ -4,7 +4,7 @@ public import DiamondExampleA.Ring.Defs
 
 namespace Ring
 
-public theorem add_left_comm [Ring α] : ∀ a b c : α, a + (b + c) = b + (a + c) := by
+public theorem poorly_named_lemma [Ring α] : ∀ a b c : α, a + (b + c) = b + (a + c) := by
   intros a b c
   rw [← add_assoc a b c]
   rw [add_comm a b]