Trying to define WellFounded.fix, universe level error

Stream: new members

[Perrin Alaine-Sedano]

Hi, I'm new to proof assistants and I'm trying to get through the exercises in Theorem Proving in Lean 4. I've gotten stuck on the one asking me to define my own version of WellFounded.fix (Exercise 3 in Section Induction and Recursion).

I couldn't figure out a way to do it with the match construct that terminated, and I saw that Acc.brecOn can only produce elements of Prop for some reason so it's not suitable for general recursion, while Acc.rec and Acc.recOn are not implemented by the code generator.

I decided to try defining my own method of structural recursion on Acc with my own below construct. Here's my attempt:

   inductive myBelow {α : Sort u} {r : α → α → Prop} {motive : {a : α} → Acc r a → Sort v} : Acc r a → Sort ((max u v) + 1) where
      | intro (a : α) {h : ∀ y, r y a → Acc r y} : (∀ (y : α) (hrya : r y a), myBelow (h y hrya)) → (∀ (y : α) (hrya : r y a  ), motive (h y hrya)) → (t : Acc r a) → myBelow t

This gives the error message

invalid universe level in constructor 'myBelow.intro', parameter has type
  (y : α) → (hrya : r y a) → motive ⋯
at universe level
  imax u v
it must be smaller than or equal to the inductive datatype universe level
  max (u+1) (v+1)

I'm really confused. Isn't imax u v always going to be a smaller or equal universe level than max (u+1) (v+1)? I think there must be some fundamental things I don't understand about how universes work in Lean, but I'm at a loss with this error.

If anyone can help me out, I'd really appreciate it. Thank you!

UPDATE: I just discovered that this error is present in version 4.14 (what I had) but is gone in 4.16. Did I just run into a recently fixed bug?

[Kyle Miller]

Yes, there were a few bugs fixed here. I'd guess #2689, #6125, or both.

[Eric Wieser]

(lean4#2689, lean4#6125)