From ed705306aeddc5682c7eeeb51fd43e2bded69501 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sat, 31 May 2025 23:02:04 -0400
Subject: [PATCH] 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                        |  6 +++
 tests/lean/run/4144.lean                      |  5 +-
 .../lean/run/invalid_field_notation_mvar.lean | 53 +++++++++++++++++++
 3 files changed, 61 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/invalid_field_notation_mvar.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 9fd49d1113..381e50ea62 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/tests/lean/run/4144.lean b/tests/lean/run/4144.lean
index f4cae530b4..783771b575 100644
--- a/tests/lean/run/4144.lean
+++ b/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
diff --git a/tests/lean/run/invalid_field_notation_mvar.lean b/tests/lean/run/invalid_field_notation_mvar.lean
new file mode 100644
index 0000000000..9aea85cf73
--- /dev/null
+++ b/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