diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index db67a44a9c..effc34879f 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1285,7 +1285,10 @@ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do
   try
     withoutMacroStackAtErr do
       if (← synthesizeCoeInstMVarCore mvarId) then
-        expandCoe <| mkAppN (Lean.mkConst ``coeSort [u, v]) #[α, β, a, mvar]
+        let result ← expandCoe <| mkAppN (Lean.mkConst ``coeSort [u, v]) #[α, β, a, mvar]
+        unless (← isType result) do
+          throwError "failed to coerse{indentExpr a}\nto a type, after applying `coeSort`, result is still not a type{indentExpr result}\nthis is often due to incorrect `CoeSort` instances, the synthesized value for{indentExpr coeSortInstType}\nwas{indentExpr mvar}"
+        return result
       else
         throwError "type expected"
   catch
diff --git a/tests/lean/621.lean b/tests/lean/621.lean
new file mode 100644
index 0000000000..40b9a4f411
--- /dev/null
+++ b/tests/lean/621.lean
@@ -0,0 +1,4 @@
+instance (ϕ : α → Prop) : CoeSort (Subtype ϕ) α where
+  coe := fun x => x.val
+
+example (ϕ : α → Prop) (xs : Subtype ϕ) (x : xs) : True := trivial
diff --git a/tests/lean/621.lean.expected.out b/tests/lean/621.lean.expected.out
new file mode 100644
index 0000000000..9617102f41
--- /dev/null
+++ b/tests/lean/621.lean.expected.out
@@ -0,0 +1,9 @@
+621.lean:4:45-4:47: error: type expected
+failed to coerse
+  xs
+to a type, after applying `coeSort`, result is still not a type
+  xs.val
+this is often due to incorrect `CoeSort` instances, the synthesized value for
+  CoeSort (Subtype ϕ) α
+was
+  instCoeSortSubtype ϕ