From 3b58a7d36b73b2ea7536d92b767ce0dbab3618fb Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Tue, 15 Jul 2025 17:32:59 -0400
Subject: [PATCH] fix: improve error message when projecting from zero-field
 type (#9386)

This PR improves a confusing error message that occurred when attempting
to project from a zero-field structure.

Closes #9312
---
 src/Lean/Elab/App.lean   |  3 +++
 tests/lean/run/9312.lean | 31 +++++++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 tests/lean/run/9312.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 0dd8f86686..90098bad1f 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1301,6 +1301,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
             So, we don't projection functions for it. Thus, we use `Expr.proj` -/
           return LValResolution.projIdx structName (idx - 1)
       else
+        if numFields == 0 then
+          throwLValError e eType m!"Invalid projection: Projections are not supported on this type \
+            because it has no fields"
         let (fields, bounds) := if numFields == 1 then
           (m!"field", m!"the only valid index is 1")
         else
diff --git a/tests/lean/run/9312.lean b/tests/lean/run/9312.lean
new file mode 100644
index 0000000000..eef6939b8e
--- /dev/null
+++ b/tests/lean/run/9312.lean
@@ -0,0 +1,31 @@
+/-!
+# Projections on types without fields
+
+https://github.com/leanprover/lean4/issues/9312
+
+Ensures that a suitable error message is displayed when attempting to project from a type that has
+no fields.
+-/
+
+structure MyEmpty where
+
+/--
+error: Invalid projection: Projections are not supported on this type because it has no fields
+  { }
+has type
+  MyEmpty
+-/
+#guard_msgs in
+#check (MyEmpty.mk).1
+
+inductive T where
+  | a
+
+/--
+error: Invalid projection: Projections are not supported on this type because it has no fields
+  T.a
+has type
+  T
+-/
+#guard_msgs in
+#check (T.a).1