From e618a0a4f505ed2e51bfeff2753bf89eb474908a Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sat, 31 May 2025 23:00:46 -0400
Subject: [PATCH] fix: invalid dotted identifier notation error for sort
 (#8260)

This PR clarifies the invalid dotted identifier notation error when the
type is a sort.

Co-authored-by @sgraf812.

---------

Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
---
 src/Lean/Elab/App.lean                        | 22 ++++++++-------
 .../run/invalid_dotted_identifier_prop.lean   | 27 +++++++++++++++++++
 2 files changed, 40 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/invalid_dotted_identifier_prop.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index e1053fcd19..9fd49d1113 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1506,15 +1506,19 @@ where
     let resultTypeFn := resultType.cleanupAnnotations.getAppFn
     try
       tryPostponeIfMVar resultTypeFn
-      let .const declName .. := resultTypeFn.cleanupAnnotations
-        | throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
-      let idNew := declName ++ id.getId.eraseMacroScopes
-      if (← getEnv).contains idNew then
-        mkConst idNew
-      else if let some (fvar, []) ← resolveLocalName idNew then
-        return fvar
-      else
-        throwUnknownIdentifierAt id m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+      match resultTypeFn.cleanupAnnotations with
+      | .const declName .. =>
+        let idNew := declName ++ id.getId.eraseMacroScopes
+        if (← getEnv).contains idNew then
+          mkConst idNew
+        else if let some (fvar, []) ← resolveLocalName idNew then
+          return fvar
+        else
+          throwUnknownIdentifierAt id m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+      | .sort .. =>
+        throwError "Invalid dotted identifier notation: not supported on type{indentExpr resultTypeFn}"
+      | _ =>
+        throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
     catch
       | ex@(.error ..) =>
         match (← unfoldDefinition? resultType) with
diff --git a/tests/lean/run/invalid_dotted_identifier_prop.lean b/tests/lean/run/invalid_dotted_identifier_prop.lean
new file mode 100644
index 0000000000..f702152ee2
--- /dev/null
+++ b/tests/lean/run/invalid_dotted_identifier_prop.lean
@@ -0,0 +1,27 @@
+/--
+error: Invalid dotted identifier notation: not supported on type
+  Prop
+-/
+#guard_msgs in
+def foo (n : Nat) : Nat :=
+  match n < 42 with
+  | .true => n
+  | .false => 47
+
+/--
+error: Invalid dotted identifier notation: not supported on type
+  Sort ?u.44
+-/
+#guard_msgs in
+def foo2 (n : Nat) : Nat :=
+  match PUnit with
+  | .unit => n
+
+def Prop.true := True
+
+/--
+error: Invalid dotted identifier notation: not supported on type
+  Prop
+-/
+#guard_msgs in
+#check (.true : Prop)