Understanding equation compiler trace and errors

Stream: general

[Ramon Fernandez Mir]

I was trying to define Picard iteration on real-valued functions, which only involves ℝ and ℕ. So I was quite shocked when the error I got was VM does not have code for 'ennreal.canonically_ordered_comm_semiring'. mwe:

import measure_theory.interval_integral

open nat

set_option trace.eqn_compiler true

def P.recursive (x₀ : ℝ) (f : ℝ → ℝ → ℝ) : ℕ → ℝ → ℝ
| 0        := λ t, x₀
| (succ n) := λ t, x₀ + (∫ s in 0..t, f s (P.recursive n s))
/-
equation compiler failed to generate bytecode for 'P.recursive._main'
nested exception message:
code generation failed, VM does not have code for 'ennreal.canonically_ordered_comm_semiring'
-/

/-
[eqn_compiler] compiling
def P.recursive : ℕ → ℝ → ℝ
| 0 := λ (t : ℝ), x₀
| n.succ := λ (t : ℝ), x₀ + ∫ (s : ℝ) in 0..t, f s (P.recursive n s)
[eqn_compiler] recursive:          1
[eqn_compiler] nested recursion:   0
[eqn_compiler] using_well_founded: 0
[eqn_compiler] using unbounded recursion (meta-definition):
...
-/

def P.recursive' (x₀ : ℝ) (f : ℝ → ℝ → ℝ) : ℕ → ℝ → ℝ :=
λ n, nat.rec_on n
    (λ t, x₀)
    (λ m Pm, λ t, x₀ + (∫ s in 0..t, f s (Pm s)))
/-
definition 'P.recursive'' is noncomputable, it depends on 'interval_integral'
-/

Using nat.rec_on, I get the error I expected, as clearly the problem with these definitions is that they should be marked as noncomputable. Why did I get an error about ennreal? Is it used in unbounded recursion?

[Ramon Fernandez Mir]

Also what do the numbers 1, 0, 0 next to recursive, nested recursive, etc. mean??

[Johan Commelin]

measures take values in ennreal, I guess that's how they get involved.

[Ramon Fernandez Mir]

Aha! That makes more sense. Thanks