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

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.

Start by loading the reproducer and comparing ex2 with the working ex1, ex3, ex4, and ex5 cases. Investigate the elaboration and kernel type-checking path for the implicit coercion from set to Sort. Done means ex2 produces no kernel type-checking error while the existing cases remain valid.