typeclass inference not seeing through reducible definition

Stream: lean4

[Kevin Buzzard]

In Lean 3 this works:

-- Lean 3
universes w v u

class Category (V : Type u) :=
(Hom : V → V → Sort v)

instance : Category (Type u) :=
{ Hom := λ v w, v → w }

open Category

universes u₁ v₁ u₂ v₂

structure Functor' (V : Type u₁) [Category.{v₁} V] (W : Type u₂) [Category.{v₂} W]

infixr ` ⥤ `:26 := Functor'       -- type as \func --

variables (C : Type u) [Category.{v} C]

def Functor.id : C ⥤ C := {}

notation `𝟭` := Functor.id -- Type this as `\sb1`

class ConcreteCategory (C : Type u) [Category.{v} C] :=
(Forget : C ⥤ Type w)

@[reducible]
def forget (C : Type u) [Category.{v} C] [ConcreteCategory.{w} C] : C ⥤ Type w :=
  ConcreteCategory.Forget

instance ConcreteCategory.types : ConcreteCategory (Type u) :=
{ Forget := 𝟭 _ }

class ReflectsLimits {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (F : C ⥤ D)

instance idReflectsLimits {C : Type u} [Category.{v} C] : ReflectsLimits (𝟭 C) := {}

example : ReflectsLimits (forget (Type u)) := idReflectsLimits -- works

example : ReflectsLimits (forget (Type u)) := infer_instance -- works

In particular typeclass inference can solve ReflectsLimits (forget (Type u)) (and does, in mathlib). The analogous Lean 4 code doesn't work:

-- Lean 4
universe w v u

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

instance : Category (Type u) where
  Hom := λ v w => v → w

open Category

structure Functor' (V : Type u₁) [Category.{v₁} V] (W : Type u₂) [Category.{v₂} W] where

infixr:26 " ⥤ " => Functor' -- type as \func

variable (C : Type u) [Category.{v} C]

def Functor.id : C ⥤ C where

notation "𝟭" => Functor.id -- Type this as `\sb1`

class ConcreteCategory (C : Type u) [Category.{v} C] where
  /-- We have a functor to Type -/
  Forget : C ⥤ Type w

@[reducible]
def forget (C : Type u) [Category.{v} C] [ConcreteCategory.{w} C] : C ⥤ Type w :=
  ConcreteCategory.Forget

instance ConcreteCategory.types : ConcreteCategory (Type u) where
  Forget := 𝟭 _

class ReflectsLimits {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (F : C ⥤ D) where

instance idReflectsLimits {C : Type u} [Category.{v} C] : ReflectsLimits (𝟭 C) where

example : ReflectsLimits (forget (Type u)) := idReflectsLimits -- works

#synth ReflectsLimits (forget (Type u)) -- fails

Is there some way I can make things more [reducible] or something, in order to get this to work? The point is that forget (Type u) is defeq to 𝟭 _ and forget is reducible, but it's not enough in Lean 4. If I can't get this working somehow then I'm going to have to add a bunch of instances to some file in the port to work around this, which is certainly a solution but it's kind of a last resort.

[Adam Topaz]

Adding reducible to literally everything in this file doesn't seem to work. So I guess the answer is no, it's not possible?

[Adam Topaz]

Maybe there's some unification hint that would make this work? Let me try

[Adam Topaz]

oops: https://leanprover.github.io/lean4/doc/unifhint.html?highlight=hint#unification-hints

[Adam Topaz]

I realized I don't actually know how to make unification hints :(

[Kevin Buzzard]

Maybe it's just the same as in Lean 3! Did you know how to do it in Lean 3? (I certainly didn't...)

[Adam Topaz]

No, I didn't :see_no_evil:

[Adam Topaz]

Okay, I don't have time to try to figure out how (or if) unification hints can help here. But I think it would be very interesting to see whether they do actually solve this issue! Hopefully someone who knows what they're doing with unification hints can help?

[Kevin Buzzard]

Here's how they work @Adam Topaz :

structure Magma where
  α : Type
  mul : α → α → α

infixl:70 (priority := high) "**" => Magma.mul _

-- #check (3 : Nat) ** (3 : Nat) -- fails

def Nat.Magma : Magma where
  α := Nat
  mul a b := Nat.mul a b

unif_hint (S : Magma) where
  S ≟ Nat.Magma ⊢ S.α ≟ Nat

#check (3 : Nat) ** (3 : Nat) -- works

[Eric Wieser]

Kevin Buzzard said:

Maybe it's just the same as in Lean 3! Did you know how to do it in Lean 3? (I certainly didn't...)

I think in Lean3 they only worked in Type 0

[Eric Wieser]

Adam Topaz said:

Adding reducible to literally everything in this file doesn't seem to work. So I guess the answer is no, it's not possible?

attribute [reducible] ConcreteCategory.Forget ConcreteCategory.types works

[Scott Morrison]

@Kevin Buzzard, I think for your example to make sense, you should move the failing #check below def Nat.Magma!

[Scott Morrison]

Do you have a good heuristic for remembering in

unif_hint where
  W ≟ X ⊢ Y ≟ Z

the respective roles of W X Y Z? It seems from your example that one should read this as "if you are trying to match Z with Y, instead try match X with W", which is disconcertingly right-to-left! :-)

[Kevin Buzzard]

Moving the check to just after Nat.magma doesn't make it work, fortunately :-) It seems that it's possible to swap Y,Z and also X,W. I'm just putting together the very little stuff that other people have written about unification hints, I have no more understanding of what's going on than you.

[Adam Topaz]

@Kevin Buzzard that’s the sort of example I actually did figure out :) Leo mentioned this example (and related ones) in his ICERM talk, for example. But I still couldn’t figure out how to make progress with the ReflectLimits issue above unification hints. Could you find some way to make that work?

@Eric Wieser I thought I tied that as well, but maybe I’m misremembering. In any case, it’s not clear to me whether tagging things as reducible is the right approach in this case.

[Eric Wieser]

I think it's sensible to make defs that resolve to types reducible

[Eric Wieser]

In lean3 we got away with not doing so because TC search would (sometimes) ignore reducibility and reduce things anyway

[Eric Wieser]

!4#3857