Debugging notation scope

Stream: mathlib4

[Brendan Seamas Murphy]

I made a change somewhere that breaks Mathlib.CategoryTheory.Bicategory.Adjunction, specifically it errors at the definition of the identity adjunction between identities with the message

ambiguous, possible interpretations
  𝟙 a ⊣ 𝟙 a : Type w

  ?m.185637 ⊣ ?m.185790 : Type (max (max (max ?u.185368 ?u.185367) ?u.185370) ?u.185369)

My interpretation of this error message is that the second ⊣ is CategoryTheory.Adjunction, and so a change I made in some ancestor file caused that notation come into scope here. What tools are there for debugging this? Is there some way to trace when in the history of my imports the notation first comes into scope?

[Kyle Miller]

What's the notation you're using that's expanding into these?

[Kyle Miller]

It would be nice if this error message would tell you what syntax you started with that got you here, but it only reports the expansions, which isn't so useful for the first step of debugging.

[Kyle Miller]

Oh, never mind, it does give you the syntax. It all depends on how the notation works, and whether it generated a delaborator...

[Kyle Miller]

The tool I know is to do a global search for " ⊣ "

[Kyle Miller]

(That's with the quotes by the way)

[Brendan Seamas Murphy]

Hm I guess I don't actually want the first place it comes into scope since that's just going to be the definition site (and I know where that is). Now I'm not sure what exactly I'd like to search for

[Kyle Miller]

At least you can figure out that the bicategory version only comes into scope if you're in or opened the CategoryTheory.Bicategory namespace.

[Kyle Miller]

It's ok having ambiguous notation by the way -- you just need to give enough type information so that the elaborator can disambiguate.

[Brendan Seamas Murphy]

Well that's not really a concern at the moment, the bicategory version is defined 9 lines prior to this error message

[Brendan Seamas Murphy]

Kyle Miller said:

It's ok having ambiguous notation by the way -- you just need to give enough type information so that the elaborator can disambiguate.

Right, I'm just not sure what change I made that turned this instance ambiguous

[Brendan Seamas Murphy]

I haven't touched any of the bicategory files, just monoidal category stuff

[Brendan Seamas Murphy]

Huh, the issue was a stack of coercions from monoidal functors to lax monoidal functors to functors. Not sure how that broke things