Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC