bug in the builtin elaborator

Stream: general

[Eric Wieser]

This lemma:

import data.set.finite

lemma foo {α : Type*} {s : set α} (h : set.finite s) [decidable_eq (h.to_finset : set α)] :
  true := trivial

is giving me the error

kernel failed to type check declaration 'foo' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {α : Type u_1} {s : set α} (h : s.finite) [_inst_1 : decidable_eq ↥↑(h.to_finset)], true
elaborated value:
  λ {α : Type u_1} {s : set α} (h : s.finite) [_inst_1 : decidable_eq ↥↑(h.to_finset)], trivial
nested exception message:
type mismatch at application
  decidable_eq ↥↑(h.to_finset)
term
  ↥↑(h.to_finset)
has type
  has_coe_to_sort.S (set α)
but is expected to have type
  Sort u_2

In the absence of any tactics, this must be an elaborator bug, right?

[Kevin Buzzard]

If you're looking for a fix, then coercing manually does the job:

import data.set.finite

universe u

lemma foo {α : Type u} {s : set α} (h : set.finite s) [decidable_eq ((h.to_finset : set α) : Type u)] :
  true := trivial

[Kevin Buzzard]

You don't need finsets:

import data.set.finite

universe u

lemma foo {α : Type u} {s : set α} [decidable_eq s] :
  true := trivial -- works

lemma bar {α : Type u} {s : set α} [decidable_eq (s : set α)] :
  true := trivial -- fails (same error)

[Mario Carneiro]

It appears that the elaborator is inferring this:

instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, λ s, {x // x ∈ s}⟩
universes u v
variable {α : Type u}
lemma bar {s : set α} [decidable_eq.{v} (s : set α)] : true := trivial -- fails (kernel error)

That is, the universe variable on decidable_eq is a fresh universe v unrelated to the type of anything in sight. The kernel is complaining that it should be u+1, and if you put decidable_eq.{u+1} it works. Perhaps the has_coe_to_sort is getting resolved too late and the universe constraint is never applied?

[Mario Carneiro]

(The fact that the above definition is also accepted by the elaborator despite the type error appears to be a variant on the same issue.)