meta mutual def errors

Stream: general

[Mario Carneiro]

Does anyone know the source of this error? I get unexpected error, failed to generate equational lemmas in the front-end even though it's a meta def so it shouldn't have equations

meta mutual def A, B
with A : unit → tactic unit | _ := return ()
with B : unit → tactic unit | _ := return ()

[Scott Morrison]

(Mario and I are sitting next to each other and just discovered the curious answer. I'll explain while he does something useful. :-)

[Scott Morrison]

This doesn't work:

meta mutual def A, B
with A : ℕ → ℕ
| n := 0
with B : ℕ → ℕ
| n := 0

[Scott Morrison]

with the same error.

[Scott Morrison]

However

meta mutual def A, B
with A : ℕ → ℕ
| 0 := 0
| (n+1) := B 0
with B : ℕ → ℕ
| n := 0

[Scott Morrison]

or even

meta mutual def A, B
with A : ℕ → ℕ
| 0 := 0
| (n+1) := A 0
with B : ℕ → ℕ
| n := 0

[Scott Morrison]

Somehow the compiler is insisting that the definitions actually refer to either themselves or each other.

[Scott Morrison]

And this only happens in meta.

[Scott Morrison]

Oh well! :-)