Bytecode warning when defining a yoneda-like functor

Stream: general

[Dagur Asgeirsson]

What does this error message even mean? From previous discussions here on Zulip I understand that this often occurs when something that's not a Prop is called lemma and not def, but that's not the case here.

def fin_yoneda (X : Type (u+1)) : Fintype.{u}ᵒᵖ  ⥤ Type (u+1) :=
{ obj := λ Y, (unop Y) → X,
  map := λ Y Z f g z, g (f.unop z) }
  /-
  failed to generate bytecode for 'fin_yoneda'
  infer type failed, function expected at
    f z
  term
    f
  has type
    Y ⟶ Z
  -/

[Yaël Dillies]

What does adding noncomputable do?

[Dagur Asgeirsson]

Nothing :(

[Dagur Asgeirsson]

Well I have a "noncomputable theory" at the top, and removing it does nothing

[Yaël Dillies]

It looks like it's just having trouble seeing that f : Y ⟶ Z is a function. What if you type-ascript?

[Dagur Asgeirsson]

Like this? It gives the same error.

def fin_yoneda (X : Type (u+1)) : Fintype.{u}ᵒᵖ  ⥤ Type (u+1) :=
{ obj := λ Y, (unop Y) → X,
  map := λ Y Z f g z, g ((f.unop : (unop Z) → (unop Y)) z) }

[Dagur Asgeirsson]

f itself is of course not a function, it's an arrow in the opposite category

[Yaël Dillies]

What's the type of all the variables? Can we have a MWE?

[Dagur Asgeirsson]

The only variable is X : Type (u+1).

[Dagur Asgeirsson]

What's even weirder is that my_yoneda defined below gives the same error message, yet my_yoneda_eq_yoneda is true:

def my_yoneda (X : Type (u+1)) : (Type (u+1))ᵒᵖ ⥤ Type (u+1) :=
{ obj := λ Y, unop Y ⟶ X,
  map := λ Y Y' f g, f.unop ≫ g }

lemma my_yoneda_eq_yoneda (X : Type (u+1)) : my_yoneda X = yoneda.obj X := by refl

[Yaël Dillies]

Dagur Ásgeirsson said:

The only variable is X : Type (u+1).

No, but f, g, etc... Can you copy the context or, better, give us a #mwe?

[Dagur Asgeirsson]

Here is a mwe:

import category_theory.yoneda
import category_theory.Fintype

universe u

open opposite
open category_theory

def my_yoneda (X : Type (u+1)) : (Type (u+1))ᵒᵖ ⥤ Type (u+1) :=
{ obj := λ Y, unop Y ⟶ X,
  map := λ Y Y' f g, f.unop ≫ g }

lemma my_yoneda_eq_yoneda (X : Type (u+1)) : my_yoneda X = yoneda.obj X := by refl

def fin_yoneda (X : Type (u+1)) : Fintype.{u}ᵒᵖ  ⥤ Type (u+1) :=
{ obj := λ Y, (unop Y) → X,
  map := λ Y Z f g z, g ((f.unop : (unop Z) → (unop Y)) z) }

[Dagur Asgeirsson]

Y, Z, f, g, z are all bound by the lambda but here is the state after it in fin_yoneda:

X : Type (u+1),
Y Z : Fintypeᵒᵖ,
f : Y ⟶ Z,
g : ↥(unop Y) → X,
z : ↥(unop Z)
⊢ X

[Jon Eugster]

I have no clue about anything here, but I find it interesting that the following seems to work although I would naively expect it to do the same thing:

import category_theory.yoneda
import category_theory.Fintype

universe u

open opposite

def fin_yoneda (X : Type (u+1)) : Fintype.{u}ᵒᵖ  ⥤ Type (u+1) :=
{ obj := λ Y, (unop Y) → X,
  map := λ Y Z f g z, begin
    let f' := (f.unop),
    exact g (f' z),
  end
}

[Eric Wieser]

def my_yoneda (X : Type (u+1)) : (Type (u+1))ᵒᵖ ⥤ Type (u+1) :=
{ obj := λ Y, unop Y ⟶ X,
  map := λ Y Y' f g, let f' := f.unop in f' ≫ g }

works too

[Dagur Asgeirsson]

Thanks, that's weird. Would be interesting if someone knows why this works

[Kyle Miller]

Dagur Ásgeirsson said:

Well I have a "noncomputable theory" at the top, and removing it does nothing

The Lean 3 noncomputability logic is:

• If the function is marked noncomputable!, believe the user and skip the rest of these steps.
• Determine whether the function should be computable or not.
• If there's no noncomputable theory at the top, complain if the user got it wrong (i.e., if they put or didn't put noncomputable on this definition correctly).

[Kyle Miller]

This means that if you have noncomputable theory, Lean completely(*) ignores whether you put noncomputable or not.

(*) Just to complicate things, the equation compiler acts differently depending on whether you add noncomputable. I think this only really impacts recursive definitions.

[Dagur Asgeirsson]

Hmm ok, putting noncomputable! works:

noncomputable! def fin_yoneda (X : Type (u+1)) : Fintype.{u}ᵒᵖ  ⥤ Type (u+1) :=
{ obj := λ Y, (unop Y) → X,
  map := λ Y Z f g z, g (f.unop z), }

[Kyle Miller]

(deleted: you tried my suggestion already! :racecar:)

[Kyle Miller]

Oh, this is a fascinating error:

failed to generate bytecode for 'my_yoneda'
infer type failed, function expected at
  f x
term
  f
has type
  Y ⟶ Y'

[Kyle Miller]

I'm not going to go and debug it, but I have a strong suspicion what it is. opposite is @[irreducible], and the core infer_type algorithm doesn't unfold irreducible definitions when calculating the type. I don't think this error should happen, but I doubt it will be fixed in Lean 3.

[Kyle Miller]

Here's what set_option trace.compiler true reveals about how this function is transformed during compilation:

λ (X : Type (u+1)),
  {obj := λ (Y : (Type (u+1))ᵒᵖ), unop Y → X,
   map := λ (Y Y' : (Type (u+1))ᵒᵖ) (f : Y ⟶ Y') (g : unop Y ⟶ X) (x : unop Y'), g (f x),
   map_id' := my_yoneda._proof_1 X,
   map_comp' := my_yoneda._proof_2 X}

[Eric Wieser]

I think the definition of docs#quiver.hom.unop is to blame

[Kyle Miller]

It inlines the definition of ≫ for the Type category and simplifies some things until it gets to g (f x), but f isn't a function that can be applied due to irreducibility.

[Kyle Miller]

Yeah, it looks like it's inlining hom.unop but with irreducibility thrown in it's not seeing it as being type correct. (I think arguably the compiler should be able to handle this though.)

[Eric Wieser]

hom.unop should presumably be implemented in terms of composition with op and unop?

[Eric Wieser]

Kyle Miller said:

but I have a strong suspicion what it is. opposite is @[irreducible]

Indeed, this fixes it

attribute [semireducible] quiver.opposite

[Kyle Miller]

I'm not sure there's any fix for hom.unop that would protect against infer_type failing

[Kyle Miller]

There's a Lean 4 issue tracking what seems to be the same problem.

[Eric Wieser]

Trying to wrap it in a structure seems to run into universe issues

[Eric Wieser]

Making quiver.opposite semireducible seems like an obvious fix

[Eric Wieser]

I don't see why it makes sense to make it irreducible, it's not guarding a type synonym or anything

[Kyle Miller]

There's a different quiver structure on Type u vs (Type u)ᵒᵖ at least, so you don't want opposite to be unfolded. It also helps protect against composing morphisms that shouldn't be composed

[Eric Wieser]

Aren't you describing why opposite should be irreducible? I don't see why quiver.opposite should be irreducible

[Eric Wieser]

That feels like making docs#mul_opposite.has_mul irreducible, which we don't do

[Kyle Miller]

Oh, I see. I think quiver.opposite being irreducible is to make it so that you can't see that the hom sets are pi types, that way you can put instances on them that are different from other pi type instances (but I don't really know the justification).

[Kyle Miller]

Here's the commit that made it irreducible: https://github.com/leanprover-community/mathlib/commit/042c290dac25b5f1c77255f1039fae301774d6cf

[Eric Wieser]

I'm afraid I don't see what you mean by "see that the hom sets are pi types"