fix: invalid field notation error for mvar (#8259)

This PR clarifies the invalid field notation error when projected value
type is a metavariable.

Co-authored-by @sgraf812.

---------

Co-authored-by: Sebastian Graf <sg@lean-fro.org>

src/Lean/Elab/App.lean

@@ -1191,6 +1191,12 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
     | _ => pure ()
+  else if eType.getAppFn.isMVar then
+    let field :=
+      match lval with
+      |  .fieldName _ fieldName _ _ => toString fieldName
+      | .fieldIdx _ i => toString i
+    throwError "Invalid field notation: type of{indentExpr e}\nis not known; cannot resolve field '{field}'"
   match eType.getAppFn.constName?, lval with
   | some structName, LVal.fieldIdx _ idx =>
     if idx == 0 then

tests/lean/run/4144.lean

@@ -1,8 +1,7 @@
 /--
-error: invalid field notation, type is not of the form (C ...) where C is a constant
+error: Invalid field notation: type of
   x✝
-has type
-  ?m.9
+is not known; cannot resolve field '1'
 ---
 error: unsolved goals
 case refine'_1

tests/lean/run/invalid_field_notation_mvar.lean

@@ -0,0 +1,53 @@
+structure Foo where (n : Nat)
+def Foo.f1 (f : Foo) : Nat := f.n
+def Foo.f2 (f : Foo) : Nat := f.n
+def Foo.f3 (f : Foo) : Nat := f.n
+def Foo.f4 (f : Foo) : Nat := f.n
+def Foo.f5 (f : Foo) : Nat := f.n
+
+/--
+error: Invalid field notation: type of
+  f
+is not known; cannot resolve field 'n'
+---
+error: Invalid field notation: type of
+  g
+is not known; cannot resolve field 'n'
+---
+error: Invalid field notation: type of
+  f
+is not known; cannot resolve field 'f1'
+---
+error: Invalid field notation: type of
+  g
+is not known; cannot resolve field 'f2'
+---
+error: Invalid field notation: type of
+  h
+is not known; cannot resolve field 'f3'
+---
+error: Invalid field notation: type of
+  f
+is not known; cannot resolve field 'f4'
+---
+error: Invalid field notation: type of
+  g
+is not known; cannot resolve field 'f5'
+---
+error: Invalid field notation: type of
+  h
+is not known; cannot resolve field 'f6'
+-/
+#guard_msgs in
+example := (λ f g h =>
+  let x : Foo := ⟨f.n + 1⟩;
+  let y : Foo := ⟨g.n + 1⟩;
+  (λ f g h => f.f1 + g.f2 + h.f3 + f.f4 + g.f5 + h.f6) f g h)
+
+/--
+error: Invalid field notation: type of
+  id x
+is not known; cannot resolve field 'foo'
+-/
+#guard_msgs in
+example := fun x => (id x).foo