surprising "failed to generate bytecode" warning

Stream: general

[Kevin Buzzard]

Ashvni showed me a surprising warning: here's a MWE:

import number_theory.padics.ring_homs

variables (p : ℕ) [fact (nat.prime p)]

def sets (H : Type*) := {s : set H // true}

def foo : sets (ℤ_[p]) :=
⟨(set.preimage (padic_int.appr) {id}), by trivial⟩

/-
failed to generate bytecode for 'foo'
code generation failed, VM does not have code for 'classical.choice'
-/

Both the fact that it's a subtype and the fact that we're using padic_int.appr seem to be relevant. Can this be fixed? Should she worry if it can't? It's beyond me!

[Floris van Doorn]

Did you try adding noncomputable def and/or noncomputable theory?

[Floris van Doorn]

Ah, that doesn't seem to fix it...

[Reid Barton]

I have the feeling that this mostly happens because something should be a lemma not a def or vice versa

[Reid Barton]

however, I don't see how that could apply here...

[Kevin Buzzard]

Indeed, noncomputable def complains that it should be computable. appr is defined noncomputably in number_theory.padics_ring_homs and then made irreducible on line 383, I wondered if that had anything to do with it.

[Floris van Doorn]

It somehow also has to do with the fact that set is a function into Sort*:

import number_theory.padics.ring_homs

variables (p : ℕ) [fact (nat.prime p)]

def foo {α β : Type} (f : α → β) : unit → Type := λ _, unit

def bar : {s : unit → Type // true} :=
⟨foo (@padic_int.appr p _), trivial⟩ -- error

but

import number_theory.padics.ring_homs

variables (p : ℕ) [fact (nat.prime p)]

def foo {α β : Type} (f : α → β) : Type := unit

def bar : {s : Type // true} :=
⟨foo (@padic_int.appr p _), trivial⟩ -- no error

and

import number_theory.padics.ring_homs

variables (p : ℕ) [fact (nat.prime p)]

def foo {α β : Type} (f : α → β) : unit → ℕ := λ _, 0

noncomputable def bar : {s : unit → ℕ // true} :=
⟨foo (@padic_int.appr p _), trivial⟩ -- no error (but noncomputable is mandatory)

[Eric Wieser]

Is it possible my PR to remove noncomputable lemma from docs#classical.dec is to blame?

[Eric Wieser]

I thought we were safe because mathlib was happy

[Kyle Miller]

Kevin Buzzard said:

/-
failed to generate bytecode for 'foo'
code generation failed, VM does not have code for 'classical.choice'
-/

Both the fact that it's a subtype and the fact that we're using padic_int.appr seem to be relevant. Can this be fixed? Should she worry if it can't? It's beyond me!

I've just found a strange fix for this:

import number_theory.padics.ring_homs

variables (p : ℕ) [fact (nat.prime p)]

def sets (H : Type*) := {s : set H // true}

local attribute [inline] set.preimage

def foo : sets (ℤ_[p]) :=
⟨(set.preimage (padic_int.appr) {id}), by trivial⟩

I think it's got to do with the fact that the vm doesn't see that padic_int.appr is computationally irrelevant for some reason. But once it's expanded out to

def foo' : sets (ℤ_[p]) :=
⟨{x | padic_int.appr x ∈ ({id} : set (ℕ → ℕ))}, by trivial⟩

then it's happy.