polymorphism and `derive decidable_eq`

Stream: new members

[Horatiu Cheval]

When doing a non-polymorphic definition, derive decidable_eq works fine in the following example. However, defining pnat as a Type u instead of a Type or a Type 37 breaks it. Why does this happens, what difference does adding a universe variable makes for derive?
I don't get much from the error message: injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor

universes u

@[derive decidable_eq]
inductive pnat : Type u
| zero : pnat
| succ : pnat → pnat

[Kevin Buzzard]

universes u

@[derive decidable_eq]
inductive pnat : Type u
| zero : pnat
| succ : pnat → pnat

example (a : pnat) := if a = pnat.zero then tt else ff -- works fine for me

[Kevin Buzzard]

Are you on current mathlib master?

[Horatiu Cheval]

Wait, it's weird. Your code works for me too, but mine was originally in a section, and if I place it in a section then it doesn't work:

section

  universes u

  @[derive decidable_eq]
  inductive pnat : Type u
  | zero : pnat
  | succ : pnat → pnat

end

[Horatiu Cheval]

Sorry for not posting this initially , I didn't imagine the section could have anything to do it