Debugging typeclass inference

Stream: mathlib4

[Dagur Asgeirsson]

#6847 causes an error "tactic 'aesop' failed, failed to prove the goal after exhaustive search" in pullbackDiagonalMapIso which lives in Mathlib/CategoryTheory/Limits/Shapes/Diagonal, a file I didn't touch.

That definition has an argument [HasPullbacks C], and I define a new class HasPullbacksOfInclusions for categories and add instance [HasPullbacks C] : HasPullbacksOfInclusions C. It's definitely my instance that is causing the error, even though I've reduced its priority to 1. I just don't know exactly how, and I'm wondering how to debug things like this.

[Scott Morrison]

Without actually looking at your code, your instance sounds fine. While you're right to be cautious about replacing an aesop proof with a manual one, it's possible that it's reasonable here...

[Dagur Asgeirsson]

Ok well it's definitely the instance that's causing the failure, because if I remove it the aesop proof works fine

[Dagur Asgeirsson]

I've added a manual proof of that theorem. Apparently this wasn't the only error though, now I get "PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:839:14: unknown metavariable" in Mathlib/AlgebraicGeometry/OpenImmersion/Basic. How do I debug this?

[Kevin Buzzard]

I don't think you debug panics, I think you post some code which panics on master and then ask someone else to please fix it :-)

[Dagur Asgeirsson]

Never mind, I'm redoing this PR in a slightly different way and I'll put my instances in new files instead