feat: hint when an autobound variable's type fails to be a function or equality

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.