failed to synthesize CategoryStruct

Stream: new members

[Shanghe Chen]

Hi in an exercise related to bundle category and bicategory I reach the following error:

import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.ConcreteCategory.Bundled

noncomputable section
set_option autoImplicit false
universe w v u
open CategoryTheory Functor

instance (H: Bundled Category.{w, v}): Category.{w, v} H := H.str

structure BBC1 (B : Type u) where
  Hom : B → B → Type v
  homCategory : ∀ a b : B, Category.{w} (Hom a b)
  testInst {a b: B} (f: Hom a b) : f ⟶ f

def test1 {B: Type u} (bc: ∀ X Y: B, Bundled Category.{w, v}) : BBC1 B where
  Hom X Y := bc X Y
  homCategory X Y := by infer_instance
  testInst f := 𝟙 f

structure BBC2 (B : Type u) extends Quiver.{v+1} B where
  homCategory : ∀ a b : B, Category.{w} (Hom a b)
  testInst (a b: B) (f: Hom a b) : f ⟶ f

def test2 {B: Type u} (bc: ∀ X Y: B, Bundled Category.{w, v}) : BBC2  B where
  Hom X Y := bc X Y
  -- here cannot infer_instance
  homCategory X Y := (bc X Y).str
  /-
  failed to synthesize
    CategoryStruct.{w, v} (X ⟶ Y)
  use `set_option diagnostics true` to get diagnostic information
  -/
  testInst X Y f := 𝟙 f

def test3 {B: Type u} (b : ∀ X Y : B, Type v) (bc: ∀ X Y: B, Category.{w, v} (b X Y)) : BBC2 B where
  Hom X Y := b X Y
  -- here cannot infer_instance
  homCategory X Y := (bc X Y)
  testInst X Y f := 𝟙 f

[Shanghe Chen]

both test1 and test3 work in the above code, whereas test2 failed with error

  failed to synthesize
    CategoryStruct.{w, v} (X ⟶ Y)
  use `set_option diagnostics true` to get diagnostic information

I am not getting why test2 failed to synthesize the instance, which I think it should be from homCategory as test3

[Shanghe Chen]

In the same time both test2 and test3 fail to use infer_instance like test1. I cannot get why infer_instance failed in these two def too

[Shanghe Chen]

The only difference between BBC1 and BBC2 seems to be BBC2 defines Hom via extending Quiver while BBC1 defines it directly as a field.

[Shanghe Chen]

Setting set_option diagnostics true as the error suggests gives

[reduction] unfolded declarations (max: 29, num: 1): ▼
  Quiver.Hom ↦ 29
[reduction] unfolded instances (max: 29, num: 2): ▼
  Category.toCategoryStruct ↦ 29
  CategoryStruct.toQuiver ↦ 21
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

and I still have no clue on it

[Shanghe Chen]

I found that the following workaround using test3 for test2

def test4 {B: Type u} (bc: ∀ X Y: B, Bundled Category.{w, v}) : BBC2 B :=
    test3 (fun X Y => (bc X Y).α)
       (fun X Y => (bc X Y).str)

[Shanghe Chen]

Also it can be done with

def test2 {B: Type u} (bc: ∀ X Y: B, Bundled Category.{w, v}) : BBC2  B where
  Hom X Y := (bc X Y).α
  -- here cannot infer_instance
  homCategory X Y := (bc X Y).str
  testInst X Y f := @CategoryStruct.id (bc X Y) (bc X Y).str.toCategoryStruct f

the .toCategoryStruct part cannot be omitted. Being unable to synthesize it as typeclass still kind of weird to me