debugging TC synth failure

Stream: mathlib4

[Johan Commelin]

Can someone recommend a next step in debugging this failure? (This is from a branch...)

instance (X : Cᵒᵖ) : RingHomId (R.map (𝟙 X)) where
  eq_id := by rw [R.map_id X]; rfl

instance (X : Cᵒᵖ) : RingHomId (R.map (𝟙 X)) := inferInstance -- works

set_option trace.Meta.synthInstance true

@[simp]
theorem map_id (P : PresheafOfModules R) (X : Cᵒᵖ) :
    P.map (𝟙 X) = LinearMap.id' := by
                  -- failed to synthesize instance RingHomId ⇑(R.map (𝟙 X))
  ext
  simp
-- [Meta.synthInstance] ❌ RingHomId ⇑(R.map (𝟙 X)) ▼
--   [] no instances for RingHomId ⇑(R.map (𝟙 X)) ▼
--     [instances] #[]

[Johan Commelin]

In particular, how can I get more info from Lean why it thinks there are no instances? Clearly there is an instance a few lines up. (And this instance works when provided manually.)

[Adam Topaz]

your code seems to work as is for me?

[Johan Commelin]

Right, because I didn't give you my branch. I'll push it now.

[Johan Commelin]

branch#jmc-comp-triples

[Matthew Ballard]

What’s the imports?

[Johan Commelin]

The problem occurs halfway the file Mathlib/Algebra/Category/ModuleCat/Presheaf.lean on that branch.

[Matthew Ballard]

It is trying to coerce from a ring hom whereas the instance is coercing from a function.

[Johan Commelin]

Can you tell me how you found that?

[Matthew Ballard]

Expanding the term coming from the instance and expanding what was expected at the failure

[Matthew Ballard]

I can’t really dig anymore at the moment

[Johan Commelin]

Ok, I think I understand what you mean:

• the instance is using RingCat.instFunLike under the hood, whereas
• the failure expects something using RingHom.instFunLike.

Those two are defeq, but Lean probably doesn't get a chance to realize that.

[Matthew Ballard]

Oh right! Sorry \to and \hom look almost the same now in nvim

[Johan Commelin]

I guess this note is relevant:

instance instFunLike {X Y : RingCat} : FunLike (X ⟶ Y) X Y :=
  -- Note: this is apparently _not_ defeq to RingHom.instFunLike with reducible transparency
  ConcreteCategory.instFunLike

[Johan Commelin]

And I should point out:

example (R S : RingCat) : @RingCat.instFunLike R S = RingHom.instFunLike := rfl -- works

[Adam Topaz]

Can we just put Homs of RingCat et al. in a structure wrapper already?

[Johan Commelin]

Part of me is a bit sad if that is necessary, but maybe it's the path of least resistance.

[Adam Topaz]

The path of more resistance would be to unbundle homs from Category.

[Adam Topaz]

or maybe make certain things reducible in a clever way which isn't obvious to me.

[Johan Commelin]

This works, but it's an ugly convert hack.

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
index 572cc07091..6a36a907ec 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@@ -62,37 +62,22 @@ theorem map_apply (P : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x) :
     P.map f x = (P.presheaf.map f) x :=
   rfl

-instance (X : Cᵒᵖ) : RingHomId (R.map (𝟙 X)) where
+instance ringHomId (X : Cᵒᵖ) : RingHomId (R.map (𝟙 X)) where
   eq_id := by rw [R.map_id X]; rfl

-instance {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :
+instance ringHomCompTriple {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :
     RingHomCompTriple (R.map f) (R.map g) (R.map (f ≫ g)) where
   comp_eq := by rw [R.map_comp f g]; rfl

 @[simp]
 theorem map_id (P : PresheafOfModules R) (X : Cᵒᵖ) :
-    P.map (𝟙 X) = LinearMap.id' := by
+    P.map (𝟙 X) = by convert LinearMap.id'; apply ringHomId := by
   ext
   simp

 @[simp]
 theorem map_comp (P : PresheafOfModules R) {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :
-    P.map (f ≫ g) = (P.map g).comp (P.map f) := by
+    P.map (f ≫ g) = by convert (P.map g).comp (P.map f); apply ringHomCompTriple := by
   ext
   simp

[Adam Topaz]

I suppose RingHom.comp (P.map g) (P.map f) should also work instead of convert ...?

[Matthew Ballard]

Got a little time. Let me poke at the reducible and instances defeq failure

[Johan Commelin]

I opened #11590 with this changes.

[Johan Commelin]

Feel free to push to that branch

[Johan Commelin]

The goal is to refactor RingHomCompTriple so that it no longer talks about ring homs, but just any functions. Then the infrastructure can be reused for other kinds of equivariant homs.

[Johan Commelin]

@Antoine Chambert-Loir needs something like that for #6057

[Matthew Ballard]

It won’t unfold CategoryTheory.forget RingCat

[Matthew Ballard]

Strange

[Matthew Ballard]

Here is a default transparency successful trace

[Meta.isDefEq] ✅ RingCat.instFunLike =?= RingHom.instFunLike ▼
  [] ✅ RingCat.instFunLike =?= { coe := fun f ↦ f.toFun, coe_injective' := ⋯ } ▼
    [] ✅ CategoryTheory.ConcreteCategory.instFunLike =?= { coe := fun f ↦ f.toFun, coe_injective' := ⋯ } ▼
      [] ✅ { coe := fun f ↦ (CategoryTheory.forget RingCat).map f,
            coe_injective' := ⋯ } =?= { coe := fun f ↦ f.toFun, coe_injective' := ⋯ } ▼
        [] ✅ fun f ↦ (CategoryTheory.forget RingCat).map f =?= fun f ↦ f.toFun ▼
          [] ✅ R ⟶ S =?= ↑R →+* ↑S ▼
            [] ✅ CategoryTheory.CategoryStruct.toQuiver.1 R S =?= ↑R →+* ↑S ▼
              [] ✅ CategoryTheory.BundledHom.MapHom SemiRingCat.AssocRingHom (@Ring.toSemiring) R.str S.str =?= ↑R →+* ↑S ▼
                [] ✅ SemiRingCat.AssocRingHom ↑R ↑S =?= ↑R →+* ↑S ▼
                  [] ✅ ↑R →+* ↑S =?= ↑R →+* ↑S
          [] ✅ (CategoryTheory.forget RingCat).map f =?= f.toFun ▼
            [] ✅ (CategoryTheory.forget RingCat).toPrefunctor.2 f =?= (↑↑f).1 ▼
              [] ✅ (CategoryTheory.BundledHom.bundledHomOfParentProjection SemiRingCat.AssocRingHom @Ring.toSemiring).toFun R.str S.str
                    f =?= (↑↑f).1 ▼
                [] ✅ (CategoryTheory.BundledHom.bundledHomOfParentProjection SemiRingCat.AssocRingHom @Ring.toSemiring).1 R.str S.str
                      f =?= (↑↑f).1 ▼
                  [] ✅ SemiRingCat.bundledHom.toFun Ring.toSemiring Ring.toSemiring f =?= (↑↑f).1 ▼
                    [] ✅ SemiRingCat.bundledHom.1 Ring.toSemiring Ring.toSemiring f =?= (↑↑f).1 ▼
                      [] ✅ ⇑f =?= (↑↑f).1 ▼
                        [] ✅ RingHom.instFunLike.1 f =?= (↑↑f).1 ▼
                          [] ✅ f.toFun =?= (↑↑f).1 ▼
                            [] ✅ (↑↑f).1 =?= (↑↑f).1 ▼
                              [] ✅ ↑↑f =?= ↑↑f ▼
                                [] ✅ (↑f).1 =?= (↑f).1 ▼
                                  [] ✅ ↑f =?= ↑f ▼
                                    [] ✅ f.1 =?= f.1
        [] ✅ R ⟶ S =?= ↑R →+* ↑S
        [] ✅ (CategoryTheory.forget RingCat).obj R =?= ↑R ▼
          [] ✅ (CategoryTheory.forget RingCat).toPrefunctor.1 R =?= R.1 ▼
            [] ✅ ↑R =?= R.1 ▼
              [] ✅ R.1 =?= R.1
        [] ✅ fun x ↦ (CategoryTheory.forget RingCat).obj S =?= fun x ↦ ↑S ▼
          [] ✅ (CategoryTheory.forget RingCat).obj R =?= ↑R
          [] ✅ (CategoryTheory.forget RingCat).obj S =?= ↑S ▼
            [] ✅ (CategoryTheory.forget RingCat).toPrefunctor.1 S =?= S.1 ▼
              [] ✅ ↑S =?= S.1 ▼
                [] ✅ S.1 =?= S.1

[Matthew Ballard]

Versus the unsuccessful with_reducible_and_instances rfl

[Meta.isDefEq] ❌ RingCat.instFunLike =?= RingHom.instFunLike ▼
  [] ❌ RingCat.instFunLike =?= { coe := fun f ↦ f.toFun, coe_injective' := ⋯ } ▼
    [] ❌ CategoryTheory.ConcreteCategory.instFunLike =?= { coe := fun f ↦ f.toFun, coe_injective' := ⋯ } ▼
      [] ❌ { coe := fun f ↦ (CategoryTheory.forget RingCat).map f,
            coe_injective' := ⋯ } =?= { coe := fun f ↦ f.toFun, coe_injective' := ⋯ } ▼
        [] ❌ fun f ↦ (CategoryTheory.forget RingCat).map f =?= fun f ↦ f.toFun ▼
          [] ✅ R ⟶ S =?= ↑R →+* ↑S ▼
            [] ❌ @Quiver.Hom =?= RingHom
            [onFailure] ❌ R ⟶ S =?= ↑R →+* ↑S
            [] ✅ CategoryTheory.BundledHom.MapHom SemiRingCat.AssocRingHom (@Ring.toSemiring) R.str S.str =?= ↑R →+* ↑S ▼
              [] ✅ SemiRingCat.AssocRingHom ↑R ↑S =?= ↑R →+* ↑S ▼
                [] ✅ ↑R →+* ↑S =?= ↑R →+* ↑S
          [] ❌ (CategoryTheory.forget RingCat).map f =?= f.toFun ▼
            [] ❌ (CategoryTheory.forget RingCat).toPrefunctor.2 f =?= (↑↑f).1 ▼
              [onFailure] ❌ (CategoryTheory.forget RingCat).toPrefunctor.2 f =?= (↑↑f).1

[Matthew Ballard]

This is a possibility

instance bundledHom : BundledHom AssocRingHom where
  toFun _ _ f := f
  id _ := RingHom.id _
  comp _ _ _ f g := f.comp g

[Matthew Ballard]

I see two non-reducible declarations in there

[Matthew Ballard]

No it is most likely non-reducibility of RingCat

[Matthew Ballard]

Hmm. Nope

[Matthew Ballard]

Well I fixed it Nevermind the error wasn’t highlighted

[Matthew Ballard]

Apparently you can delete deriving for LargeCategory RingCat and nothing between there and this file breaks

[Johan Commelin]

Lol, crazy mathlib facts you're spitting there (-;

[Matthew Ballard]

Ok now I think I really did fix it. Make RingCat reducible and then ConcreteCategory RingCat becomes a inferInstance but you need to change the proof to that. Or you can just get rid of the explicit LargeCategory and ConcreteCategory instances since Lean can find them with RingCat reducible

[Matthew Ballard]

And duh. That deletion I mentioned only works because I made RingCat reducible

[Matthew Ballard]

It seems fine to make RingCat reducible since it wraps Bundled Ring which is a structure instance

[Matthew Ballard]

I guess one should check performance to be safe

[Matthew Ballard]

Unfortunately it still doesn’t fix the error you originally presented since Bundled.\a is not reducible (I think)

[Matthew Ballard]

Making that reducible doesn’t help

[Johan Commelin]

Hmmz, ok. So maybe the conclusion should be that these lemmas are crossing API boundaries?

[Matthew Ballard]

I certainly think cleaner boundaries would help

[Matthew Ballard]

Here is _a_ fix to the original problem given the above is already implemented:

def bizzle (X : Cᵒᵖ) : R.obj X →+* R.obj X := R.map (𝟙 X)

instance (X : Cᵒᵖ) : RingHomId (bizzle (R := R) X) where
  eq_id := sorry

[Matthew Ballard]

I haven’t tried to disentangle the two things

[Matthew Ballard]

#11595 makes SemiRingCat and RingCat reducible. Performance impact currently being assessed

[Matthew Ballard]

At worst neutral