strange error (universe issue?)

Stream: general

[Heather Macbeth]

The following gives an error when marked as a lemma, though not when marked as an example:

import data.finset.basic

example {α : Type*} (s : finset α) (hs' : set.nonempty (s : set α)) : nonempty (s : set α) :=
hs'.to_subtype

lemma test {α : Type*} (s : finset α) (hs' : set.nonempty (s : set α)) : nonempty (s : set α) :=
hs'.to_subtype

The error message is

type mismatch, term
  hs'.to_subtype
has type
  nonempty.{(max 1 (u_1+1))}
    (@coe_sort.{(max (u_1+1) 1) (max 1 (u_1+1))+1} (set.{u_1} α) (@set.has_coe_to_sort.{u_1} α)
       (@coe.{u_1+1 (max (u_1+1) 1)} (finset.{u_1} α) (set.{u_1} α)
          (@coe_to_lift.{u_1+1 (max (u_1+1) 1)} (finset.{u_1} α) (set.{u_1} α) (@finset.set.has_coe_t.{u_1} α))
          s))
but is expected to have type
  nonempty.{u_2}
    (@coe_sort.{(max (u_1+1) 1) (max 1 (u_1+1))+1} (set.{u_1} α) (@set.has_coe_to_sort.{u_1} α)
       (@coe.{u_1+1 (max (u_1+1) 1)} (finset.{u_1} α) (set.{u_1} α)
          (@coe_to_lift.{u_1+1 (max (u_1+1) 1)} (finset.{u_1} α) (set.{u_1} α) (@finset.set.has_coe_t.{u_1} α))
          s))

which seems to suggest a universe issue (that's the only difference between the two types, as far as I can tell).

Any ideas for fixing it?

[Reid Barton]

It looks like a Lean bug. The expected type does not type check. Try changing the proof to sorry!

[Reid Barton]

A workaround:

universe u

lemma test {α : Type u} (s : finset α) (hs' : set.nonempty (s : set α)) : nonempty.{u+1} (s : set α) :=
hs'.to_subtype

[Heather Macbeth]

Reid Barton said:

It looks like a Lean bug. The expected type does not type check. Try changing the proof to sorry!

Indeed, that moves the bug elsewhere!

kernel failed to type check declaration 'test' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {α : Type u_1} (s : finset α), ↑s.nonempty → nonempty ↥↑s
elaborated value:
  λ {α : Type u_1} (s : finset α) (hs' : ↑s.nonempty), sorry
nested exception message:
type mismatch at application
  nonempty ↥↑s
term
  ↥↑s
has type
  has_coe_to_sort.S (set α)
but is expected to have type
  Sort u_2

[Heather Macbeth]

Your workaround works perfectly, so I will use that.

[Heather Macbeth]

Is the Lean "bug" actually a bug, or just a failure to exhibit the behaviour one would naively expect?