Specify error explanation more specifically

Author: robsimmons

src/Lean/Elab/App.lean

@@ -1375,25 +1375,27 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\
       has function type{inlineExprTrailing eType}"
 
-  | .mvar .., lval =>
-    let (notationKind, _, projKind, projName) := getLValDesc lval
-    throwError m!"Invalid {notationKind}: Type of{indentExpr e}\nis not known; cannot resolve {projKind} `{projName}`"
+  | .mvar .., .fieldName _ fieldName _ _ =>
+    throwNamedError lean.invalidField m!"Invalid field notation: Type of{indentExpr e}\nis not \
+      known; cannot resolve field `{fieldName}`"
+  | .mvar .., .fieldIdx _ i  =>
+    throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
+      projection `{i}`"
 
   | _, _ =>
     match e.getAppFn, lval with
     | Expr.const c _, .fieldName _ref _fieldName (some suffix) _fullRef =>
       throwUnknownConstant (c ++ suffix)
-    | _, _ =>
-      let (notationKind, notationDesc, _, _) := getLValDesc lval
-      throwNamedError lean.invalidField m!"Invalid {notationKind}: {notationDesc} operates on \
-      types of the form `C ...` where C is a constant. The expression{indentExpr e}\nhas \
-      type{inlineExpr eType}which does not have the necessary form."
+    | _, .fieldName .. =>
+      throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \
+        types of the form `C ...` where C is a constant. The expression{indentExpr e}\nhas \
+        type{inlineExpr eType}which does not have the necessary form."
+    | _, .fieldIdx _ i =>
+      throwError  m!"Invalid projection: Projection operates on types of the form `C ...` where C \
+        is a constant. The expression{indentExpr e}\nhas type{inlineExpr eType}which does not have \
+        the necessary form."
 
 where
-  getLValDesc : LVal → String × String × String × String
-  | .fieldName _ fieldName _ _  => ("field notation", "Field projection", "field", s!"{fieldName}")
-  | .fieldIdx _ i => ("projection", "Projection", "projection", s!"{i}")
-
   throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
       (declHint := Name.anonymous) : TermElabM α := do
     let msg ←
@@ -1403,9 +1405,8 @@ where
           possible to project the field `{fieldName}` from an expression{indentExpr e}\nof \
           type{inlineExprTrailing eType}"
     -- By using `mkUnknownIdentifierMessage`, the tag `Lean.unknownIdentifierMessageTag` is
-    -- incorporated tag included within the message, as required for the "import unknown identifier"
-    -- code action. The "outermost" lean.invalidField name is the only one that triggers an error
-    -- explanation.
+    -- incorporated within the message, as required for the "import unknown identifier" code action.
+    -- The "outermost" lean.invalidField name is the only one that triggers an error explanation.
     throwNamedErrorAt ref lean.invalidField msg
 
 

src/Lean/ErrorExplanations/InvalidField.lean

@@ -27,7 +27,9 @@ and be a calling a function on the value `color` with
 #eval (4 + 2).suc
 ```
 ```output
-Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression `4 + 2` of type `Nat`
+Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression
+  4 + 2
+of type `Nat`
 ```
 ```lean fixed
 #eval (4 + 1).succ
@@ -41,7 +43,9 @@ The simplest reason fo
 #eval '>'.leftpad 10 ['a', 'b', 'c']
 ```
 ```output
-Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression `'>'` of type `Char`
+Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression
+  '>'
+of type `Char`
 ```
 ```lean fixed
 #eval ['a', 'b', 'c'].leftpad 10 '>'
@@ -51,17 +55,16 @@ The type of the expression before the dot determines the function being called b
 the dot. There is no `Char.leftpad`, and the only way to invoke `List.leftpad` with generalized
 field notation is to have the list come before the dot.
 
-## Insufficient Type Information
+## Type is Not Specific
 
 ```lean broken
 def double_plus_one {α} [Add α] (x : α) :=
    (x + x).succ
 ```
 ```output
-Invalid field notation: Type is not of the form `C ...` where C is a constant
+Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
   x + x
-has type
-  α
+has type `α` which does not have the necessary form.
 ```
 ```lean fixed
 def double_plus_one (x : Nat) :=
@@ -71,6 +74,23 @@ def double_plus_one (x : Nat) :=
 The `Add` typeclass is sufficient to for the addition `x + x`, but the `.succ` field notation
 cannot operate without knowing more about the actual type from which `succ` is being projected.
 
+## Insufficient Type Information
+
+```lean broken
+example := fun (n) => n.succ.succ
+```
+```output
+Invalid field notation: Type of
+  n
+is not known; cannot resolve field `succ`
+```
+```lean fixed
+example := fun (n : Nat) => n.succ.succ
+```
+
+Generalized field notation can only be used when it is possible to determine the type that is being
+projected. Type annotations may therefore need to be added to make generalized field notation work.
+
 -/
 register_error_explanation lean.invalidField {
   summary := "Dotted identifier notation used without ."