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