trace class errors

trace.txt

The code that produced this trace was:

import ring_theory.ideals

set_option trace.class_instances true
def is_fg {α β} [ring α] [module α β]
  (s : set β) [is_submodule s] : Prop :=
∃ t : finset β, _root_.span (t : set β)  = s

at some point where there was a dodgy instance (since fixed). The error was a typeclass loop caused by line 8.

*******************************

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_3 : has_coe_to_fun (finset β) := @finsupp.has_coe_to_fun ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_fun (finset β) := @cau_seq.has_coe_to_fun ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_fun (finset β) := @applicative_transformation.has_coe_to_fun ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_fun (finset β) := @function.has_coe_to_fun ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_fun (finset β) := @equiv.has_coe_to_fun ?x_21 ?x_22
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_fun (finset β) := @expr.has_coe_to_fun ?x_23
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_fun (finset β) := @coe_fn_trans ?x_24 ?x_25 ?x_26 ?x_27
[class_instances] (1) ?x_26 : has_coe_t_aux (finset β) ?x_25 := @coe_base_aux ?x_28 ?x_29 ?x_30
[class_instances] (2) ?x_30 : has_coe (finset β) ?x_29 := @quotient_ring.has_coe ?x_31 ?x_32 ?x_33 ?x_34
[class_instances] (3) ?x_32 : comm_ring (finset β) := @quotient_ring.comm_ring ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (3) ?x_32 : comm_ring (finset β) := rat.comm_ring
failed is_def_eq
[class_instances] (3) ?x_32 : comm_ring (finset β) := @cau_seq.comm_ring ?x_39 ?x_40 ?x_41 ?x_42 ?x_43 ?x_44
failed is_def_eq
[class_instances] (3) ?x_32 : comm_ring (finset β) := @nonzero_comm_ring.to_comm_ring ?x_45 ?x_46
[class_instances] (4) ?x_46 : nonzero_comm_ring (finset β) := @quotient_ring.nonzero_comm_ring ?x_47 ?x_48 ?x_49 ?x_50
failed is_def_eq
[class_instances] (4) ?x_46 : nonzero_comm_ring (finset β) := rat.nonzero_comm_ring
failed is_def_eq
[class_instances] (4) ?x_46 : nonzero_comm_ring (finset β) := @integral_domain.to_nonzero_comm_ring ?x_51 ?x_52
[class_instances] (5) ?x_52 : integral_domain (finset β) := @quotient_ring.integral_domain ?x_53 ?x_54 ?x_55 ?x_56
failed is_def_eq
[class_instances] (5) ?x_52 : integral_domain (finset β) := rat.integral_domain
failed is_def_eq
[class_instances] (5) ?x_52 : integral_domain (finset β) := @field.to_integral_domain ?x_57 ?x_58
[class_instances] (6) ?x_58 : field (finset β) := rat.field
failed is_def_eq
[class_instances] (6) ?x_58 : field (finset β) := @linear_ordered_field.to_field ?x_59 ?x_60
[class_instances] (7) ?x_60 : linear_ordered_field (finset β) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (7) ?x_60 : linear_ordered_field (finset β) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_61 ?x_62
[class_instances] (8) ?x_62 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (6) ?x_58 : field (finset β) := @discrete_field.to_field ?x_59 ?x_60
[class_instances] (7) ?x_60 : discrete_field (finset β) := rat.discrete_field
failed is_def_eq
[class_instances] (7) ?x_60 : discrete_field (finset β) := @discrete_linear_ordered_field.to_discrete_field ?x_61 ?x_62
[class_instances] (8) ?x_62 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_52 : integral_domain (finset β) := @discrete_field.to_integral_domain ?x_53 ?x_54 ?x_55
[class_instances] (6) ?x_54 : discrete_field (finset β) := rat.discrete_field
failed is_def_eq
[class_instances] (6) ?x_54 : discrete_field (finset β) := @discrete_linear_ordered_field.to_discrete_field ?x_56 ?x_57
[class_instances] (7) ?x_57 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_52 : integral_domain (finset β) := @linear_ordered_comm_ring.to_integral_domain ?x_53 ?x_54
[class_instances] (6) ?x_54 : linear_ordered_comm_ring (finset β) := rat.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_54 : linear_ordered_comm_ring (finset β) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_55 ?x_56
[class_instances] (7) ?x_56 : decidable_linear_ordered_comm_ring (finset β) := rat.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_56 : decidable_linear_ordered_comm_ring (finset β) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_57 ?x_58 ?x_59 ?x_60
[class_instances] (7) ?x_56 : decidable_linear_ordered_comm_ring (finset β) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (7) ?x_56 : decidable_linear_ordered_comm_ring (finset β) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_57 ?x_58
[class_instances] (8) ?x_58 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (3) ?x_32 : comm_ring (finset β) := int.comm_ring
failed is_def_eq
[class_instances] (3) ?x_32 : comm_ring (finset β) := @field.to_comm_ring ?x_35 ?x_36
[class_instances] (4) ?x_36 : field (finset β) := rat.field
failed is_def_eq
[class_instances] (4) ?x_36 : field (finset β) := @linear_ordered_field.to_field ?x_37 ?x_38
[class_instances] (5) ?x_38 : linear_ordered_field (finset β) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_38 : linear_ordered_field (finset β) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_39 ?x_40
[class_instances] (6) ?x_40 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (4) ?x_36 : field (finset β) := @discrete_field.to_field ?x_37 ?x_38
[class_instances] (5) ?x_38 : discrete_field (finset β) := rat.discrete_field
failed is_def_eq
[class_instances] (5) ?x_38 : discrete_field (finset β) := @discrete_linear_ordered_field.to_discrete_field ?x_39 ?x_40
[class_instances] (6) ?x_40 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (3) ?x_32 : comm_ring (finset β) := @integral_domain.to_comm_ring ?x_35 ?x_36
[class_instances] (4) ?x_36 : integral_domain (finset β) := @quotient_ring.integral_domain ?x_37 ?x_38 ?x_39 ?x_40
failed is_def_eq
[class_instances] (4) ?x_36 : integral_domain (finset β) := rat.integral_domain
failed is_def_eq
[class_instances] (4) ?x_36 : integral_domain (finset β) := @field.to_integral_domain ?x_41 ?x_42
[class_instances] (5) ?x_42 : field (finset β) := rat.field
failed is_def_eq
[class_instances] (5) ?x_42 : field (finset β) := @linear_ordered_field.to_field ?x_43 ?x_44
[class_instances] (6) ?x_44 : linear_ordered_field (finset β) := rat.linear_ordered_field
failed is_def_eq
[class_instances] (6) ?x_44 : linear_ordered_field (finset β) := @discrete_linear_ordered_field.to_linear_ordered_field ?x_45 ?x_46
[class_instances] (7) ?x_46 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_42 : field (finset β) := @discrete_field.to_field ?x_43 ?x_44
[class_instances] (6) ?x_44 : discrete_field (finset β) := rat.discrete_field
failed is_def_eq
[class_instances] (6) ?x_44 : discrete_field (finset β) := @discrete_linear_ordered_field.to_discrete_field ?x_45 ?x_46
[class_instances] (7) ?x_46 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (4) ?x_36 : integral_domain (finset β) := @discrete_field.to_integral_domain ?x_37 ?x_38 ?x_39
[class_instances] (5) ?x_38 : discrete_field (finset β) := rat.discrete_field
failed is_def_eq
[class_instances] (5) ?x_38 : discrete_field (finset β) := @discrete_linear_ordered_field.to_discrete_field ?x_40 ?x_41
[class_instances] (6) ?x_41 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (4) ?x_36 : integral_domain (finset β) := @linear_ordered_comm_ring.to_integral_domain ?x_37 ?x_38
[class_instances] (5) ?x_38 : linear_ordered_comm_ring (finset β) := rat.linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_38 : linear_ordered_comm_ring (finset β) := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_39 ?x_40
[class_instances] (6) ?x_40 : decidable_linear_ordered_comm_ring (finset β) := rat.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_40 : decidable_linear_ordered_comm_ring (finset β) := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_41 ?x_42 ?x_43 ?x_44
[class_instances] (6) ?x_40 : decidable_linear_ordered_comm_ring (finset β) := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (6) ?x_40 : decidable_linear_ordered_comm_ring (finset β) := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_41 ?x_42
[class_instances] (7) ?x_42 : discrete_linear_ordered_field (finset β) := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (2) ?x_30 : has_coe (finset β) ?x_29 := @quotient_module.has_coe ?x_31 ?x_32 ?x_33 ?x_34 ?x_35 ?x_36
[class_instances] (3) ?x_33 : ring ?x_31 := _inst_1
[class_instances] (3) ?x_34 : @module α (finset β) _inst_1 := _inst_2
failed is_def_eq
[class_instances] (3) ?x_34 : @module α (finset β) _inst_1 := @quotient_module.quotient.module ?x_37 ?x_38 ?x_39 ?x_40 ?x_41 ?x_42
failed is_def_eq
[class_instances] (3) ?x_34 : @module α (finset β) _inst_1 := @lc.module ?x_43 ?x_44 ?x_45 ?x_46
failed is_def_eq
[class_instances] (3) ?x_34 : @module α (finset β) _inst_1 := @vector_space.to_module ?x_47 ?x_48 ?x_49 ?x_50
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_51 : field α := rat.field
failed is_def_eq
[class_instances] (0) ?x_51 : field α := @linear_ordered_field.to_field ?x_52 ?x_53
[class_instances] (1) ?x_53 : linear_ordered_field α := rat.linear_ordered_field
failed is_def_eq
[class_instances] (1) ?x_53 : linear_ordered_field α := @discrete_linear_ordered_field.to_linear_ordered_field ?x_54 ?x_55
[class_instances] (2) ?x_55 : discrete_linear_ordered_field α := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (0) ?x_51 : field α := @discrete_field.to_field ?x_52 ?x_53
[class_instances] (1) ?x_53 : discrete_field α := rat.discrete_field
failed is_def_eq
[class_instances] (1) ?x_53 : discrete_field α := @discrete_linear_ordered_field.to_discrete_field ?x_54 ?x_55
[class_instances] (2) ?x_55 : discrete_linear_ordered_field α := rat.discrete_linear_ordered_field
failed is_def_eq
failed is_def_eq
[class_instances] (3) ?x_34 : @module α (finset β) _inst_1 := @ring.to_module ?x_51 ?x_52
failed is_def_eq
[class_instances] (3) ?x_33 : ring ?x_31 := @cau_seq.ring ?x_37 ?x_38 ?x_39 ?x_40 ?x_41 ?x_42
[class_instances] (4) ?x_38 : discrete_linear_ordered_field ?x_37 := rat.discrete_linear_ordered_field
[class_instances] (4) ?x_40 : ring ?x_39 := _inst_1
[class_instances] (4) ?x_42 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_41 := @abs_is_absolute_value ?x_43 ?x_44
failed is_def_eq
[class_instances] (4) ?x_40 : ring ?x_39 := @cau_seq.ring ?x_43 ?x_44 ?x_45 ?x_46 ?x_47 ?x_48
[class_instances] (5) ?x_44 : discrete_linear_ordered_field ?x_43 := rat.discrete_linear_ordered_field
[class_instances] (5) ?x_46 : ring ?x_45 := _inst_1
[class_instances] (5) ?x_48 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_47 := @abs_is_absolute_value ?x_49 ?x_50
failed is_def_eq
[class_instances] (5) ?x_46 : ring ?x_45 := @cau_seq.ring ?x_49 ?x_50 ?x_51 ?x_52 ?x_53 ?x_54
[class_instances] (6) ?x_50 : discrete_linear_ordered_field ?x_49 := rat.discrete_linear_ordered_field
[class_instances] (6) ?x_52 : ring ?x_51 := _inst_1
[class_instances] (6) ?x_54 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_53 := @abs_is_absolute_value ?x_55 ?x_56
failed is_def_eq
[class_instances] (6) ?x_52 : ring ?x_51 := @cau_seq.ring ?x_55 ?x_56 ?x_57 ?x_58 ?x_59 ?x_60
[class_instances] (7) ?x_56 : discrete_linear_ordered_field ?x_55 := rat.discrete_linear_ordered_field
[class_instances] (7) ?x_58 : ring ?x_57 := _inst_1
[class_instances] (7) ?x_60 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_59 := @abs_is_absolute_value ?x_61 ?x_62
failed is_def_eq
[class_instances] (7) ?x_58 : ring ?x_57 := @cau_seq.ring ?x_61 ?x_62 ?x_63 ?x_64 ?x_65 ?x_66
[class_instances] (8) ?x_62 : discrete_linear_ordered_field ?x_61 := rat.discrete_linear_ordered_field
[class_instances] (8) ?x_64 : ring ?x_63 := _inst_1
[class_instances] (8) ?x_66 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_65 := @abs_is_absolute_value ?x_67 ?x_68
failed is_def_eq
[class_instances] (8) ?x_64 : ring ?x_63 := @cau_seq.ring ?x_67 ?x_68 ?x_69 ?x_70 ?x_71 ?x_72
[class_instances] (9) ?x_68 : discrete_linear_ordered_field ?x_67 := rat.discrete_linear_ordered_field
[class_instances] (9) ?x_70 : ring ?x_69 := _inst_1
[class_instances] (9) ?x_72 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_71 := @abs_is_absolute_value ?x_73 ?x_74
failed is_def_eq
[class_instances] (9) ?x_70 : ring ?x_69 := @cau_seq.ring ?x_73 ?x_74 ?x_75 ?x_76 ?x_77 ?x_78
[class_instances] (10) ?x_74 : discrete_linear_ordered_field ?x_73 := rat.discrete_linear_ordered_field
[class_instances] (10) ?x_76 : ring ?x_75 := _inst_1
[class_instances] (10) ?x_78 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_77 := @abs_is_absolute_value ?x_79 ?x_80
failed is_def_eq
[class_instances] (10) ?x_76 : ring ?x_75 := @cau_seq.ring ?x_79 ?x_80 ?x_81 ?x_82 ?x_83 ?x_84
[class_instances] (11) ?x_80 : discrete_linear_ordered_field ?x_79 := rat.discrete_linear_ordered_field
[class_instances] (11) ?x_82 : ring ?x_81 := _inst_1
[class_instances] (11) ?x_84 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_83 := @abs_is_absolute_value ?x_85 ?x_86
failed is_def_eq
[class_instances] (11) ?x_82 : ring ?x_81 := @cau_seq.ring ?x_85 ?x_86 ?x_87 ?x_88 ?x_89 ?x_90
[class_instances] (12) ?x_86 : discrete_linear_ordered_field ?x_85 := rat.discrete_linear_ordered_field
[class_instances] (12) ?x_88 : ring ?x_87 := _inst_1
[class_instances] (12) ?x_90 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_89 := @abs_is_absolute_value ?x_91 ?x_92
failed is_def_eq
[class_instances] (12) ?x_88 : ring ?x_87 := @cau_seq.ring ?x_91 ?x_92 ?x_93 ?x_94 ?x_95 ?x_96
[class_instances] (13) ?x_92 : discrete_linear_ordered_field ?x_91 := rat.discrete_linear_ordered_field
[class_instances] (13) ?x_94 : ring ?x_93 := _inst_1
[class_instances] (13) ?x_96 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_95 := @abs_is_absolute_value ?x_97 ?x_98
failed is_def_eq
[class_instances] (13) ?x_94 : ring ?x_93 := @cau_seq.ring ?x_97 ?x_98 ?x_99 ?x_100 ?x_101 ?x_102
[class_instances] (14) ?x_98 : discrete_linear_ordered_field ?x_97 := rat.discrete_linear_ordered_field
[class_instances] (14) ?x_100 : ring ?x_99 := _inst_1
[class_instances] (14) ?x_102 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_101 := @abs_is_absolute_value ?x_103 ?x_104
failed is_def_eq
[class_instances] (14) ?x_100 : ring ?x_99 := @cau_seq.ring ?x_103 ?x_104 ?x_105 ?x_106 ?x_107 ?x_108
[class_instances] (15) ?x_104 : discrete_linear_ordered_field ?x_103 := rat.discrete_linear_ordered_field
[class_instances] (15) ?x_106 : ring ?x_105 := _inst_1
[class_instances] (15) ?x_108 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_107 := @abs_is_absolute_value ?x_109 ?x_110
failed is_def_eq
[class_instances] (15) ?x_106 : ring ?x_105 := @cau_seq.ring ?x_109 ?x_110 ?x_111 ?x_112 ?x_113 ?x_114
[class_instances] (16) ?x_110 : discrete_linear_ordered_field ?x_109 := rat.discrete_linear_ordered_field
[class_instances] (16) ?x_112 : ring ?x_111 := _inst_1
[class_instances] (16) ?x_114 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_113 := @abs_is_absolute_value ?x_115 ?x_116
failed is_def_eq
[class_instances] (16) ?x_112 : ring ?x_111 := @cau_seq.ring ?x_115 ?x_116 ?x_117 ?x_118 ?x_119 ?x_120
[class_instances] (17) ?x_116 : discrete_linear_ordered_field ?x_115 := rat.discrete_linear_ordered_field
[class_instances] (17) ?x_118 : ring ?x_117 := _inst_1
[class_instances] (17) ?x_120 : @is_absolute_value ℚ rat.discrete_linear_ordered_field α _inst_1 ?x_119 := @abs_is_absolute_value ?x_121 ?x_122
failed is_def_eq
[class_instances] (17) ?x_118 : ring ?x_117 := @cau_seq.ring ?x_121 ?x_122 ?x_123 ?x_124 ?x_125 ?x_126
[class_instances] (18) ?x_122 : discrete_linear_ordered_field ?x_121 := rat.discrete_linear_ordered_field