feat: hint when an autobound variable's type fails to be a function (#11518)

This PR provides an additional hint when the type of an autobound
implicit is required to have function type or equality type — this
fails, and the existing error message does not address the fact that the
source of the error is an unknown identifier that was automatically
bound.

## Example

```
import Lean
example : MetaM String := pure ""
```

Current error message:
```
Function expected at
  MetaM
but this term has type
  ?m

Note: Expected a function because this term is being applied to the argument
  String
```

Additional error message provided by this PR:
```
Hint: The identifier `MetaM` is unknown, and Lean's `autoImplicit` option 
causes an unknown identifier to be treated as an implicitly bound variable 
with an unknown type. However, the unknown type cannot be a function, and a 
function is what Lean expects here. This is often the result of a typo or a 
missing `import` or `open` statement.
```

Author: robsimmons

src/Lean/Elab/App.lean

@@ -245,7 +245,9 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
         .note m!"Expected a function because this term is being applied to the argument\
           {indentD <| toMessageData arg}"
       else .nil
-      throwError "Function expected at{indentExpr s.f}\nbut this term has type{indentExpr fType}{extra}"
+      throwError "Function expected at{indentExpr s.f}\nbut this term has type{indentExpr fType}\
+        {extra}\
+        {← hintAutoImplicitFailure s.f}"
 
 /-- Normalize and return the function type. -/
 private def normalizeFunType : M Expr := do

src/Lean/Elab/BuiltinNotation.lean

@@ -461,7 +461,10 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
      let heqType ← inferType heq
      let heqType ← instantiateMVars heqType
      match (← Meta.matchEq? heqType) with
-     | none => throwError "invalid `▸` notation, argument{indentExpr heq}\nhas type{indentExpr heqType}\nequality expected"
+     | none => throwError "invalid `▸` notation, argument{indentExpr heq}\n\
+        has type{indentExpr heqType}\n\
+        equality expected\
+        {← Term.hintAutoImplicitFailure heq (expected := "an equality")}"
      | some (α, lhs, rhs) =>
        let mut lhs := lhs
        let mut rhs := rhs

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,19 +36,49 @@ 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 _root_.List.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 ++ as.toOxford
+
+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.
@@ -59,7 +90,9 @@ Give alternative forms of a string if the `count` is 1 or not.
  - `(1).plural "it" "they" == "it"`
  - `(2).plural "it" "they" == "they"`
 -/
-def _root_.Nat.plural (count : Nat) (singular : String := "") (plural : String := singular ++ "s") :=
+def _root_.Nat.plural [HasPluralDefaults α] (count : Nat)
+    (singular : α := HasPluralDefaults.singular)
+    (plural : α := HasPluralDefaults.plural singular) :=
   if count = 1 then
     singular
   else

src/Lean/Elab/Term/TermElabM.lean

@@ -2169,6 +2169,16 @@ def exprToSyntax (e : Expr) : TermElabM Term := withFreshMacroScope do
   mvar.mvarId!.assign e
   return result
 
+def hintAutoImplicitFailure (exp : Expr) (expected := "a function") : TermElabM MessageData := do
+  let autoBound := (← readThe Context).autoBoundImplicitContext
+  unless autoBound.isSome && exp.isFVar && autoBound.get!.boundVariables.any (· == exp) do
+    return .nil
+  return .hint' m!"The identifier `{.ofName (← exp.fvarId!.getUserName)}` is unknown, \
+    and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly \
+    bound variable with an unknown type. \
+    However, the unknown type cannot be {expected}, and {expected} is what Lean expects here. \
+    This is often the result of a typo or a missing `import` or `open` statement."
+
 end Term
 
 open Term in

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: The identifier `m` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.

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: The identifier `MetaM` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.

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: The identifier `MetaM` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
 Nat : Type

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: The identifier `h` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be an equality, and an equality is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.

tests/lean/unknownCannotBeComplex.lean

@@ -0,0 +1,19 @@
+import Lean
+
+example : Option String := sorry
+example : Maybe String := sorry
+example : Result String Nat := sorry
+example : Nonsense String Nat := sorry
+example : MetaM String := sorry
+
+set_option relaxedAutoImplicit false in
+example : MetaM String := sorry
+
+set_option relaxedAutoImplicit false in
+example : Nonsense String := sorry
+
+example (h₁ : α = β) (as : List α) (P : List β → Type) : P (h₁ ▸ as) := sorry
+example {α β h} (h₁ : α = β) (as : List α) (P : List β → Type) : P (h ▸ as) := sorry
+example  (h₁ : α = β) (as : List α) (P : List β → Type) : P (h ▸ as) := sorry
+set_option relaxedAutoImplicit false in
+example (h₁ : α = β) (as : List α) (P : List β → Type) : P (hi ▸ as) := sorry

tests/lean/unknownCannotBeComplex.lean.expected.out

@@ -0,0 +1,59 @@
+unknownCannotBeComplex.lean:3:0-3:7: warning: declaration uses 'sorry'
+unknownCannotBeComplex.lean:4:10-4:22: error: Function expected at
+  Maybe
+but this term has type
+  ?m
+
+Note: Expected a function because this term is being applied to the argument
+  String
+
+Hint: The identifier `Maybe` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
+unknownCannotBeComplex.lean:5:10-5:27: error: Function expected at
+  Result
+but this term has type
+  ?m
+
+Note: Expected a function because this term is being applied to the argument
+  String
+
+Hint: The identifier `Result` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
+unknownCannotBeComplex.lean:6:10-6:29: error: Function expected at
+  Nonsense
+but this term has type
+  ?m
+
+Note: Expected a function because this term is being applied to the argument
+  String
+
+Hint: The identifier `Nonsense` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
+unknownCannotBeComplex.lean:7:10-7:22: error: Function expected at
+  MetaM
+but this term has type
+  ?m
+
+Note: Expected a function because this term is being applied to the argument
+  String
+
+Hint: The identifier `MetaM` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
+unknownCannotBeComplex.lean:10:10-10:15: error(lean.unknownIdentifier): Unknown identifier `MetaM`
+
+Note: It is not possible to treat `MetaM` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
+unknownCannotBeComplex.lean:13:10-13:18: error(lean.unknownIdentifier): Unknown identifier `Nonsense`
+
+Note: It is not possible to treat `Nonsense` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
+unknownCannotBeComplex.lean:15:0-15:7: warning: declaration uses 'sorry'
+unknownCannotBeComplex.lean:16:68-16:74: error: invalid `▸` notation, argument
+  h
+has type
+  ?m
+equality expected
+unknownCannotBeComplex.lean:17:61-17:67: error: invalid `▸` notation, argument
+  h
+has type
+  ?m
+equality expected
+
+Hint: The identifier `h` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be an equality, and an equality is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
+unknownCannotBeComplex.lean:19:60-19:62: error(lean.unknownIdentifier): Unknown identifier `hi`
+
+Note: It is not possible to treat `hi` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.