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

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

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)