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)