looping instances

Stream: maths

[Bhavik Mehta]

Here's the beginning of the class instances trace:

[class_instances]class-instance resolution trace
[class_instances] (0) ?x_0 : @preserves_colimit (@over C _inst_1 Z) (@over.category C _inst_1 Z) (@over C _inst_1 Y) (@over.category C _inst_1 Y) J
  _inst_2
  K
  F := @limits.comp_preserves_colimit ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12 ?x_13
failed is_def_eq
[class_instances] (0) ?x_0 : @preserves_colimit (@over C _inst_1 Z) (@over.category C _inst_1 Z) (@over C _inst_1 Y) (@over.category C _inst_1 Y) J
  _inst_2
  K
  F := @category_theory.preserves_colimit_of_creates_colimit_and_has_colimit ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20 ?x_21
  ?x_22
  ?x_23
[class_instances] (1) ?x_23 : @has_colimit J _inst_2 (@over C _inst_1 Y) (@over.category C _inst_1 Y) (K ⋙ F) := @adjunction.has_colimit_comp_equivalence ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 ?x_33
[class_instances] (2) ?x_33 : @has_colimit J _inst_2 (@over C _inst_1 Z) (@over.category C _inst_1 Z) K := @adjunction.has_colimit_comp_equivalence ?x_34 ?x_35 ?x_36 ?x_37 ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43
failed is_def_eq
[class_instances] (2) ?x_33 : @has_colimit J _inst_2 (@over C _inst_1 Z) (@over.category C _inst_1 Z) K := @over.has_colimit ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 ?x_50
[class_instances] (3) ?x_50 : @has_colimit J _inst_2 C _inst_1 (K ⋙ @over.forget C _inst_1 Z) := @adjunction.has_colimit_comp_equivalence ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58 ?x_59 ?x_60
[class_instances] (4) ?x_60 : @has_colimit J _inst_2 (@over C _inst_1 Z) (@over.category C _inst_1 Z) K := @adjunction.has_colimit_comp_equivalence ?x_61 ?x_62 ?x_63 ?x_64 ?x_65 ?x_66 ?x_67 ?x_68 ?x_69 ?x_70
failed is_def_eq
[class_instances] (4) ?x_60 : @has_colimit J _inst_2 (@over C _inst_1 Z) (@over.category C _inst_1 Z) K := @over.has_colimit ?x_71 ?x_72 ?x_73 ?x_74 ?x_75 ?x_76 ?x_77
[class_instances] (5) ?x_77 : @has_colimit J _inst_2 C _inst_1 (K ⋙ @over.forget C _inst_1 Z) := @adjunction.has_colimit_comp_equivalence ?x_78 ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84 ?x_85 ?x_86 ?x_87
[class_instances] (6) ?x_87 : @has_colimit J _inst_2 (@over C _inst_1 Z) (@over.category C _inst_1 Z) K := @adjunction.has_colimit_comp_equivalence ?x_88 ?x_89 ?x_90 ?x_91 ?x_92 ?x_93 ?x_94 ?x_95 ?x_96 ?x_97

and here's my mwe:

import category_theory.limits.over
import category_theory.adjunction

open category_theory category_theory.category category_theory.limits

universes v u
variables {C : Type u} [category.{v} C] {J : Type v} [small_category J]

set_option trace.class_instances true

example {Y Z : C} (f : Y ⟶ Z) (K : J ⥤ over Z) (F : over Z ⥤ over Y) [preserves_colimits F] : preserves_colimit K F :=
begin
  apply_instance,
end

What do I change in mathlib to fix this?

[Bhavik Mehta]

Or should I locally mark adjunction.has_colimit_comp_equivalence as not an instance

[Reid Barton]

The instance should be deleted (or made a def possibly)