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

@@ -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

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