Choice for a sum of polynomials

Stream: general

[Bolton Bailey]

Here's a minimal working error:

import data.polynomial.basic

open_locale big_operators

variables {F : Type} [field F]

def fri_poly (f : ℕ) (p : polynomial F) : ℕ -> polynomial F
| 0 := p
| (n+1) := ∑ (split : fin f), (fri_poly n)

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

How exactly does this definition depend on choice?

[Reid Barton]

Probably to add polynomials

[Eric Rodriguez]

def fri_poly (f : ℕ) (p : polynomial F) : ℕ → polynomial F
| 0 := p
| (n+1) := fri_poly n

#eval fri_poly 1 (1 : polynomial ℕ)

still fails thoguh

[Bolton Bailey]

Well ℕ is not a field

[Reid Barton]

I assume that one is due to the coercion (it probably wants to determine whether the coefficient is nonzero)

[Eric Wieser]

Fails in what way @Eric Rodriguez?

[Junyan Xu]

#eval fri_poly 1 (1 : polynomial ℚ) /- code generation failed, VM does not have code for 'classical.choice' -/
#eval fri_poly 1 (0 : polynomial ℚ) /- result type does not have an instance of type class 'has_repr', dumping internal representation (fri_poly._main (#0 #0 (_main._lambda_1)) (#0 (rat.add._main) (#0 ... (omitted) -/
I think docs#polynomial.has_one uses the classical decidability instance (via docs#finsupp.single) while docs#polynomial.has_zero doesn't.

[Kyle Miller]

code generation failed is an internal error, suggesting that the noncomputability checker is not working correctly for this example. It has to do with the equation compiler creating an auxiliary definition that needs to be compiled.

The easy short-term fix is to put noncomputable! on the definition to force everything to be noncomputable, which should hopefully work here.

[Eric Wieser]

The reason for choice here is that docs#polynomial.has_one is noncomputable