typeclass inference failure

Stream: mathlib4

[Kevin Buzzard]

I can't fix this typeclass inference failure (which worked in mathlib3) with either etaExperiment or universe annotations. What other tricks are available?

import Mathlib.CategoryTheory.ConcreteCategory.Basic

open CategoryTheory Limits

universe u₁

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

#synth ReflectsLimits.{u₁, u₁, u₁ + 1, u₁ + 1} (forget.{u₁ + 1, u₁, u₁} (Type u₁)) -- fails

example : ReflectsLimits (forget (Type u₁)) :=
  Limits.idReflectsLimits -- works, and this is an instance

example : ReflectsLimits.{u₁, u₁, u₁ + 1, u₁ + 1} (forget.{u₁ + 1, u₁, u₁} (Type u₁)) :=
  Limits.idReflectsLimits -- works

The corresponding Lean 3 code is

-- Lean 3
import category_theory.concrete_category.basic

open category_theory category_theory.limits

universe u₁

-- all works
example : reflects_limits (forget (Type u₁)) :=
by show_term {apply_instance} -- Try this: exact limits.id_reflects_limits

example : reflects_limits.{u₁ u₁ u₁ + 1 u₁ + 1} (forget.{u₁ + 1 u₁ u₁} (Type u₁)) :=
infer_instance -- works

[Kevin Buzzard]

OK so right now I have

-- porting note: these were all inferred in mathlib3
instance : ReflectsLimits (forget (Type u₁)) := Limits.idReflectsLimits
instance : PreservesColimits (forget (Type u₁)) := Limits.idPreservesColimits
instance : PreservesLimits (forget (Type u₁)) := Limits.idPreservesLimits

in a porting file (which fixes the short term problem) and am wondering if this is OK as a long term fix.

[Joël Riou]

I think it is ok to define these instances.

[Kevin Buzzard]

My worry is that there is some kind of underlying problem which we're glossing over.

[Matthew Ballard]

#synth ReflectsLimits (𝟭 (Type u₁)) -- ok
example : forget (Type u₁) = 𝟭 (Type u₁) := rfl  -- ok

Tracing the instance synthesis, shows Lean finds nothing and immediately fails for forget

[Meta.synthInstance] ❌ CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget (Type u₁)) ▼
  [] no instances for CategoryTheory.Limits.ReflectsLimitsOfSize (CategoryTheory.forget (Type u₁)) ▼
    [instances] #[]

[Kevin Buzzard]

Oh lol I hadn't engaged my brain :-) Of course it's just the identity functor! I was too busy squashing errors in a porting file to think about what was actually happening.

[Kevin Buzzard]

So this also works:

instance : ReflectsLimits (forget (Type u₁)) := by {delta forget ConcreteCategory.Forget ConcreteCategory.types; infer_instance; }

and I guess then the question is why Lean 3 was doing this automatically and Lean 4 isn't, and whether this should be fixed rather than just adding the instances I personally need to get one file compiling.

[Kevin Buzzard]

forget is marked @[reducible] and this was perhaps enough for Lean 3 typeclass inference but not for Lean 4?

[Matthew Ballard]

That would be my guess

[Matthew Ballard]

abbrev forget' := 𝟭 (Type u₁)
#synth ReflectsLimits (forget') -- ok

[Matthew Ballard]

Hmm. This is also ok

@[reducible]
def forget'' := 𝟭 (Type u₁)
#synth ReflectsLimits (forget'') -- ok

[Kevin Buzzard]

the real example needs to unfold more :-/