Recursion fails with a strange error message about universes

[JasonGross]

universes u v
inductive let_inM : Sort u → Sort (u+1)
| ret : Π {A : Sort u} , A → let_inM A
| bind : Π {A : Sort u} {B : Sort u} , let_inM A → (A → let_inM B) → let_inM B

def denote_let_inM : Π {A : Sort u} , let_inM A → A
| A (@let_inM.ret ._ v) := v
| B (@let_inM.bind A ._ v f) := let v' := @denote_let_inM A v in @denote_let_inM B (f v')
/-
-*- mode: compilation; default-directory: "~/Documents/repos/lean-playgorund/" -*-
Compilation started at Tue May 30 16:06:24

/home/jgross/Documents/repos/lean/bin/lean  /home/jgross/Documents/repos/lean-playgorund/test2.lean
/home/jgross/Documents/repos/lean-playgorund/test2.lean:6:4: error: invalid equations, when trying to recurse over reflexive inductive datatype 'let_inM' (argument #2) the universe level of the resultant universe must be zero OR not zero for every level assignment (possible solutions: provide universe levels explicitly, or force well_founded recursion by using `using_well_founded` keyword)

Compilation exited abnormally with code 1 at Tue May 30 16:06:25
-/

If I replace u with 1 and u+1 with 2, it goes through. Similarly, if I replace u with (u+1), it goes through. I'm confused what makes the equation invalid... (And should there be a warning at the datatype definition time?)

[leodemoura]

Yes, the error message is not good. The equation compiler currently uses three different strategies:

• Course of values recursion
• Well founded recursion
• Unbounded recursion (for meta definitions).

For course of values recursion, we use an auxiliary recursor (brec_on) that is automatically generated. Reflexive types such as let_inM complicate the generation of the this recursor because of impredicativity. Given A : Sort u and B : A -> Sort v, the type of Pi (a : A), B a is Sort (imax u v), where imax u v = 0 if v = 0, and imax u v = max u v otherwise. Thus, we have 1- imax u 0 = 0 2- imax u (succ v) = max u (succ v) These two identities simplify the generation of brec_on for inductive datatypes such as let_inM. To be able to use these identities we generate two versions of brec_on:

• binduction_on which can eliminate only into Prop, and where we can use identity (1) to simplify the construction, and
• brec_on which can eliminate only into data, and where we can use identity (2) to simplify the construction.

When the equation compiler tries to compile denote_let_inM, it has to decide which recursor (binduction or brec_on) to use. Since the result type may be a proposition u = 0 or not u > 0, it produces an error message. The following two variants work

namespace in_Prop
lemma denote_let_inM : Π {A : Sort 0} , let_inM A → A
| A (@let_inM.ret ._ v)      := v
| B (@let_inM.bind A ._ v f) := let v' := @denote_let_inM A v in @denote_let_inM B (f v')
end in_Prop

namespace in_data
def denote_let_inM : Π {A : Sort (u+1)} , let_inM A → A
| A (@let_inM.ret ._ v)      := v
| B (@let_inM.bind A ._ v f) := let v' := @denote_let_inM A v in @denote_let_inM B (f v')
end in_data

because in the first case the equation compiler uses binduction_on and in the second it uses brec_on.

That being said, course of values recursion is an overkill for this definition. The kernel primitive recursor rec can be used to compile it. However, we have not implemented this compilation strategy yet. This is currently on the TODO list: https://github.com/leanprover/lean/issues/1611

In the meantime, you can use the tactic framework to define def denote_let_inM : Π {A : Sort u} , let_inM A → A.

def denote_let_inM {A : Sort u} (e : let_inM A) : A :=
begin
  induction e,
  case let_inM.ret A v { exact v },
  case let_inM.bind A B v f ih_1 ih_2 { exact ih_2 ih_1 }
end

or use the recursor directly:

def denote_let_inM {A : Sort u} (e : let_inM A) : A :=
let_inM.rec 
  (λ A v, v)
  (λ A B v f ih_1 ih_2, ih_2 ih_1)
  e