fix: fixes #621

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

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

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 ϕ