Quiver C^op synthesis failure

Stream: mathlib4

[Matthew Ballard]

Why does the following #synth fail:

set_option autoImplicit false

universe w v v₁ v₂ v₃ u u₁ u₂ u₃

class Quiver (V : Type u) where
Hom : V → V → Sort v

infixr:10 " ⟶ " => Quiver.Hom

structure Opposite (α : Type u) :=
  op :: unop : α

notation:max
α "ᵒᵖ" => Opposite α

open Opposite

variable {C : Type u₁}

variable [Quiver.{v₁} C]

instance Quiver.opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun a b => (unop b ⟶ unop a)ᵒᵖ⟩

set_option trace.Meta.isDefEq true in
set_option trace.Meta.synthInstance true in
#synth Quiver Cᵒᵖ

[Matthew Ballard]

structure Opposite (α : Sort w)

fixes it

[Matthew Ballard]

So does

class Quiver (V : Type u) where
Hom : V → V → Type v

[Matthew Ballard]

What is the reason that the objects of a category are in Type u and not Sort u? I seem to remember some discussion of this before but cannot locate it

[Joël Riou]

Morphisms in quivers are allowed to be in Prop in order to allow graphs without multiple arrows.

[Matthew Ballard]

I saw that when I tried to change it and things broke fast :)

[Matthew Ballard]

But what about objects?

[Matthew Ballard]

Nothing seems to break if we do

class Quiver (V : Sort u)

[Joël Riou]

I would say there is little mathematical justification for doing this.

[Matthew Ballard]

Matthew Ballard said:

Nothing seems to break if we do

class Quiver (V : Sort u)

One thing broke ... and then everything did.

[Kevin Buzzard]

IIRC this was how it was in lean 3 -- at some point there was a refactor which allowed sorts but there were problems so they were refactored back? @Kim Morrison do you remember any more of the story?

[Kim Morrison]

Yeah, I tried it twice in the early days, both failures. I really can't remember why I want to, however. :-)

[Matthew Ballard]

Made Hom return a type and fixed enough CategoryTheory to build AlgebraicGeometry. Very anecdotal: elaboration is down about 10% for GammaSpecAdjunction which corresponds to a 5% speed up in the file.

I don't think this is the solution. I just think Lean is struggling with solving level constraints in the presence of autogenerated level metavariables

[Matthew Ballard]

This is blocking otherwise easy unifications and making it take longer, often much longer.

[Matthew Ballard]

I am also trying to create a minimized (ha!) example of the issue. But, I am learning how much AG touches