How to debug instance looping

Stream: general

[Bhavik Mehta]

I've got the error maximum class-instance resolution depth has been reached so I set set_option trace.class_instances true, and I've got a long trace. Here's the beginning of the trace:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @category_theory.limits.has_colimit J _inst_1 (@over C 𝒞 X) (@over.category_1 C 𝒞 X) F := @over.has_colimit ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6 ?x_7
[class_instances] (1) ?x_7 : @category_theory.limits.has_colimit J _inst_1 C 𝒞 (F ⋙ @over.forget C 𝒞 X) := @over.has_colimit ?x_8 ?x_9 ?x_10 ?x_11 ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (1) ?x_7 : @category_theory.limits.has_colimit J _inst_1 C 𝒞 (F ⋙ @over.forget C 𝒞 X) := @adjunction.has_colimit_comp_equivalence ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20 ?x_21 ?x_22 ?x_23 ?x_24
[class_instances] (2) ?x_24 : @category_theory.limits.has_colimit J _inst_1 (@over C 𝒞 X) (@over.category_1 C 𝒞 X) F := @over.has_colimit ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31
[class_instances] (3) ?x_31 : @category_theory.limits.has_colimit J _inst_1 C 𝒞 (F ⋙ @over.forget C 𝒞 X) := @over.has_colimit ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq

You can see the loop there - it repeats like this. How can I figure out what I've done which causes this? (If anyone wants to reproduce, clone this branch of mathlib and add import category_theory.limits.creates to the top of category_theory/limits/over.lean)

[Bhavik Mehta]

In particular what would be useful is knowing which instance is being used on each line

[Reid Barton]

The instance being matched is the one after the :=

[Bhavik Mehta]

Oh. In that case I'm more confused - none of those instances are in the new file I'm importing

[Bhavik Mehta]

Ah it's in an import of that file - thanks!