diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 3087bd867a..d137a37f6f 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index d0e748ecd4..6eb6c2dbaa 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/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
diff --git a/src/Lean/Elab/ErrorUtils.lean b/src/Lean/Elab/ErrorUtils.lean
index c9397d2801..b14e5c98de 100644
--- a/src/Lean/Elab/ErrorUtils.lean
+++ b/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,6 +36,24 @@ 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.
 
@@ -42,12 +61,24 @@ Make an oxford-comma-separated list of strings.
  - `["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
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
index 45355bf1ca..d22eb70e54 100644
--- a/src/Lean/Elab/Term/TermElabM.lean
+++ b/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
diff --git a/tests/lean/302.lean.expected.out b/tests/lean/302.lean.expected.out
index ef98a9c30f..409d33e484 100644
--- a/tests/lean/302.lean.expected.out
+++ b/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.
diff --git a/tests/lean/3989_1.lean.expected.out b/tests/lean/3989_1.lean.expected.out
index 584f740cf0..12a7ebb842 100644
--- a/tests/lean/3989_1.lean.expected.out
+++ b/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.
diff --git a/tests/lean/3989_2.lean.expected.out b/tests/lean/3989_2.lean.expected.out
index 0903b387ba..5e1952d6ae 100644
--- a/tests/lean/3989_2.lean.expected.out
+++ b/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
diff --git a/tests/lean/autoBoundPostponeLoop.lean.expected.out b/tests/lean/autoBoundPostponeLoop.lean.expected.out
index fc2a505b94..dcc8e974be 100644
--- a/tests/lean/autoBoundPostponeLoop.lean.expected.out
+++ b/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.
diff --git a/tests/lean/unknownCannotBeComplex.lean b/tests/lean/unknownCannotBeComplex.lean
new file mode 100644
index 0000000000..6a23884702
--- /dev/null
+++ b/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
diff --git a/tests/lean/unknownCannotBeComplex.lean.expected.out b/tests/lean/unknownCannotBeComplex.lean.expected.out
new file mode 100644
index 0000000000..0c62adff00
--- /dev/null
+++ b/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`.