Test: always give a warning for autobound implicits. This may be more difficult than desired.

Author: robsimmons

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/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`.