## Stream: general

### Topic: strange error (universe issue?)

#### Heather Macbeth (Dec 17 2020 at 19:46):

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 (Dec 17 2020 at 19:53):

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

#### Reid Barton (Dec 17 2020 at 19:54):

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 (Dec 17 2020 at 19:54):

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 (Dec 17 2020 at 19:55):

Your workaround works perfectly, so I will use that.

#### Heather Macbeth (Dec 17 2020 at 19:57):

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

Last updated: May 11 2021 at 22:14 UTC