"kernel failed to type check declaration" in presence of implicit coercion to Sort

[kmill]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When using a set as an argument to a class that expects a Sort, there is a "kernel failed to type check declaration" error.

Steps to Reproduce

Load the following file into Lean:

universes u
variables {α : Type u}

instance : has_coe_to_sort (set α) (Type*) := ⟨λ s, {x // x ∈ s}⟩

-- OK
lemma ex1 [inhabited α] : true := trivial

-- Not OK
lemma ex2 [inhabited (set.univ : set α)] : true := trivial
/-
kernel failed to type check declaration 'ex2' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {α : Type u} [_inst_1 : inhabited ↥set.univ], true
elaborated value:
  λ {α : Type u} [_inst_1 : inhabited ↥set.univ], trivial
nested exception message:
type mismatch at application
  inhabited ↥set.univ
term
  ↥set.univ
has type
  Type u
but is expected to have type
  Sort u_1
-/

-- OK
lemma ex3 [inhabited.{u+1} (set.univ : set α)] : true := trivial

-- OK
lemma ex4 [inhabited ↥(set.univ : set α)] : true := trivial

-- OK
lemma ex5 (s : set α) [inhabited s] : true := trivial

Expected behavior: That there are no errors.

Actual behavior: The lemma ex2 has the error listed in the above comment.

Reproduces how often: 100%

Versions

Lean 3.38.0 on Linux 5.14.12-arch1-1 #1 SMP PREEMPT Wed, 13 Oct 2021 16:58:16 +0000 x86_64 GNU/Linux

Additional Information

This might be related to #474.

This affects set.to_finset_univ in mathlib, but we are using the lemma ex4 workaround.