equation compiler complains about `classical.choice`

Stream: general

[Scott Morrison]

import data.polynomial.eval

open polynomial

def pochhammer : ℕ → polynomial ℤ
| 0 := 1
| (n+1) := X * (pochhammer n).comp(X + 1)

complains:

equation compiler failed to generate bytecode for 'pochhammer._main'
nested exception message:
code generation failed, VM does not have code for 'classical.choice'

[Scott Morrison]

Adding noncomputable theory doesn't help. What's going on?

[Yakov Pechersky]

You have to add noncomputable def. We saw this earlier with dickson polynomials:

import data.polynomial.eval
import ring_theory.polynomial.chebyshev.defs


noncomputable theory

namespace polynomial

variables {R S : Type*} [comm_ring R] [comm_ring S] (k : ℕ) (a : R)

def dickson : ℕ → polynomial R
| 0       := C ((3 : R) - k)
| 1       := X
| (n + 2) := X * dickson (n + 1) - (C a) * dickson n

The reason being, as far as my debugging let me to believe, is that the equation compiler defers labelling the whole def as noncomputable only until the end. However, since utilizing polynomial already requires noncomputable, it doesn't understand that it needs to say so just based on the inductive case. Finally, adding noncomputable theory doesn't help because that only causes an effect after the definition has been compiled. But the compiling itself is what's breaking.

[Yakov Pechersky]

Here's a simpler example:

import tactic

noncomputable theory

-- this complains!
def silly : ℕ → ℕ
| 0       := classical.some (⟨5, rfl⟩ : ∃ n, n = 5)
| (n + 1) := silly n

[Yakov Pechersky]

But this, of course, works:

def silly' : ℕ → ℕ :=
λ n, nat.rec_on n (classical.some (⟨5, rfl⟩ : ∃ n, n = 5)) (λ _ m, m)

[Yakov Pechersky]

Full example:

import tactic

noncomputable theory

-- this complains!
def silly : ℕ → ℕ
| 0       := classical.some (⟨5, rfl⟩ : ∃ n, n = 5)
| (n + 1) := silly n

noncomputable def silly_comp : ℕ → ℕ
| 0       := classical.some (⟨5, rfl⟩ : ∃ n, n = 5)
| (n + 1) := silly_comp n

def silly_rec : ℕ → ℕ :=
λ n, nat.rec_on n (classical.some (⟨5, rfl⟩ : ∃ n, n = 5)) (λ _ m, m)

#reduce silly 0
#reduce silly_comp 0
#reduce silly_rec 0
#reduce silly 1
#reduce silly_comp 1
#reduce silly_rec 1

[Bryan Gin-ge Chen]

Is lean#451 related?