subalgebra.comm_ring

Stream: maths

[Chris Hughes]

I'm getting the following type class cycle. Is there an easy solution?

[class_instances] (1) ?x_15 : comm_ring ?x_14 := @subalgebra.comm_ring ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31
[class_instances] (2) ?x_29 : comm_ring ?x_27 := @subalgebra.comm_ring ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37
[class_instances] (3) ?x_35 : comm_ring ?x_33 := @subalgebra.comm_ring ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43
[class_instances] (4) ?x_41 : comm_ring ?x_39 := @subalgebra.comm_ring ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49
[class_instances] (5) ?x_47 : comm_ring ?x_45 := @subalgebra.comm_ring ?x_50 ?x_51 ?x_52 ?x_53 ?x_54 ?x_55
[class_instances] (6) ?x_53 : comm_ring ?x_51 := @subalgebra.comm_ring ?x_56 ?x_57 ?x_58 ?x_59 ?x_60 ?x_61
[class_instances] (7) ?x_59 : comm_ring ?x_57 := @subalgebra.comm_ring ?x_62 ?x_63 ?x_64 ?x_65 ?x_66 ?x_67
[class_instances] (8) ?x_65 : comm_ring ?x_63 := @subalgebra.comm_ring ?x_68 ?x_69 ?x_70 ?x_71 ?x_72 ?x_73
[class_instances] (9) ?x_71 : comm_ring ?x_69 := @subalgebra.comm_ring ?x_74 ?x_75 ?x_76 ?x_77 ?x_78 ?x_79

[Chris Hughes]

the full message is
[class_instances] class-instance resolution trace [class_instances] (0) ?x_0 : @vector_space ℝ ℂ (@normed_field.to_discrete_field ℝ normed_field.normed_field) (@normed_group.to_add_comm_group ℂ (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field))) := @normed_space.to_vector_space ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 [class_instances] class-instance resolution trace [class_instances] (0) ?x_6 : normed_field ℝ := complex.normed_field failed is_def_eq [class_instances] (0) ?x_6 : normed_field ℝ := normed_field.normed_field [class_instances] class-instance resolution trace [class_instances] (0) ?x_7 : normed_group ℂ := @normed_ring.to_normed_group ?x_8 ?x_9 [class_instances] (1) ?x_9 : normed_ring ℂ := @normed_field.to_normed_ring ?x_10 ?x_11 [class_instances] (2) ?x_11 : normed_field ℂ := complex.normed_field [class_instances] (1) ?x_3 : normed_field ℝ := complex.normed_field failed is_def_eq [class_instances] (1) ?x_3 : normed_field ℝ := normed_field.normed_field [class_instances] (1) ?x_4 : normed_group ℂ := @normed_ring.to_normed_group ?x_12 ?x_13 [class_instances] (2) ?x_13 : normed_ring ℂ := @normed_field.to_normed_ring ?x_14 ?x_15 [class_instances] (3) ?x_15 : normed_field ℂ := complex.normed_field [class_instances] (1) ?x_5 : @normed_space ℝ ℂ normed_field.normed_field (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field)) := @fintype.normed_space ?x_16 ?x_17 ?x_18 ?x_19 ?x_20 ?x_21 ?x_22 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ normed_field.normed_field (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field)) := @prod.normed_space ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ normed_field.normed_field (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field)) := @normed_field.to_normed_space ?x_31 ?x_32 failed is_def_eq [class_instances] (3) ?x_15 : normed_field ℂ := normed_field.normed_field failed is_def_eq [class_instances] (3) ?x_15 : normed_field ℂ := @nondiscrete_normed_field.to_normed_field ?x_16 ?x_17 [class_instances] (4) ?x_17 : nondiscrete_normed_field ℂ := complex.nondiscrete_normed_field [class_instances] (1) ?x_5 : @normed_space ℝ ℂ normed_field.normed_field (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ (@nondiscrete_normed_field.to_normed_field ℂ complex.nondiscrete_normed_field))) := @fintype.normed_space ?x_18 ?x_19 ?x_20 ?x_21 ?x_22 ?x_23 ?x_24 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ normed_field.normed_field (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ (@nondiscrete_normed_field.to_normed_field ℂ complex.nondiscrete_normed_field))) := @prod.normed_space ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ normed_field.normed_field (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ (@nondiscrete_normed_field.to_normed_field ℂ complex.nondiscrete_normed_field))) := @normed_field.to_normed_space ?x_33 ?x_34 failed is_def_eq [class_instances] (4) ?x_17 : nondiscrete_normed_field ℂ := normed_field.nondiscrete_normed_field failed is_def_eq [class_instances] (2) ?x_13 : normed_ring ℂ := @prod.normed_ring ?x_14 ?x_15 ?x_16 ?x_17 failed is_def_eq [class_instances] (1) ?x_4 : normed_group ℂ := @fintype.normed_group ?x_12 ?x_13 ?x_14 ?x_15 failed is_def_eq [class_instances] (1) ?x_4 : normed_group ℂ := @prod.normed_group ?x_16 ?x_17 ?x_18 ?x_19 failed is_def_eq [class_instances] (1) ?x_3 : normed_field ℝ := @nondiscrete_normed_field.to_normed_field ?x_12 ?x_13 [class_instances] (2) ?x_13 : nondiscrete_normed_field ℝ := complex.nondiscrete_normed_field failed is_def_eq [class_instances] (2) ?x_13 : nondiscrete_normed_field ℝ := normed_field.nondiscrete_normed_field [class_instances] (1) ?x_4 : normed_group ℂ := @normed_ring.to_normed_group ?x_14 ?x_15 [class_instances] (2) ?x_15 : normed_ring ℂ := @normed_field.to_normed_ring ?x_16 ?x_17 [class_instances] (3) ?x_17 : normed_field ℂ := complex.normed_field [class_instances] (1) ?x_5 : @normed_space ℝ ℂ (@nondiscrete_normed_field.to_normed_field ℝ normed_field.nondiscrete_normed_field) (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field)) := @fintype.normed_space ?x_18 ?x_19 ?x_20 ?x_21 ?x_22 ?x_23 ?x_24 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ (@nondiscrete_normed_field.to_normed_field ℝ normed_field.nondiscrete_normed_field) (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field)) := @prod.normed_space ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ (@nondiscrete_normed_field.to_normed_field ℝ normed_field.nondiscrete_normed_field) (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field)) := @normed_field.to_normed_space ?x_33 ?x_34 failed is_def_eq [class_instances] (3) ?x_17 : normed_field ℂ := normed_field.normed_field failed is_def_eq [class_instances] (3) ?x_17 : normed_field ℂ := @nondiscrete_normed_field.to_normed_field ?x_18 ?x_19 [class_instances] (4) ?x_19 : nondiscrete_normed_field ℂ := complex.nondiscrete_normed_field [class_instances] (1) ?x_5 : @normed_space ℝ ℂ (@nondiscrete_normed_field.to_normed_field ℝ normed_field.nondiscrete_normed_field) (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ (@nondiscrete_normed_field.to_normed_field ℂ complex.nondiscrete_normed_field))) := @fintype.normed_space ?x_20 ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ (@nondiscrete_normed_field.to_normed_field ℝ normed_field.nondiscrete_normed_field) (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ (@nondiscrete_normed_field.to_normed_field ℂ complex.nondiscrete_normed_field))) := @prod.normed_space ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34 failed is_def_eq [class_instances] (1) ?x_5 : @normed_space ℝ ℂ (@nondiscrete_normed_field.to_normed_field ℝ normed_field.nondiscrete_normed_field) (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ (@nondiscrete_normed_field.to_normed_field ℂ complex.nondiscrete_normed_field))) := @normed_field.to_normed_space ?x_35 ?x_36 failed is_def_eq [class_instances] (4) ?x_19 : nondiscrete_normed_field ℂ := normed_field.nondiscrete_normed_field failed is_def_eq [class_instances] (2) ?x_15 : normed_ring ℂ := @prod.normed_ring ?x_16 ?x_17 ?x_18 ?x_19 failed is_def_eq [class_instances] (1) ?x_4 : normed_group ℂ := @fintype.normed_group ?x_14 ?x_15 ?x_16 ?x_17 failed is_def_eq [class_instances] (1) ?x_4 : normed_group ℂ := @prod.normed_group ?x_18 ?x_19 ?x_20 ?x_21 failed is_def_eq [class_instances] (0) ?x_0 : @vector_space ℝ ℂ (@normed_field.to_discrete_field ℝ normed_field.normed_field) (@normed_group.to_add_comm_group ℂ (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field))) := @continuous_linear_map.vector_space ?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 : @vector_space ℝ ℂ (@normed_field.to_discrete_field ℝ normed_field.normed_field) (@normed_group.to_add_comm_group ℂ (@normed_ring.to_normed_group ℂ (@normed_field.to_normed_ring ℂ complex.normed_field))) := @algebra.vector_space ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20 [class_instances] class-instance resolution trace [class_instances] (0) ?x_21 : ring ℂ := @normed_ring.to_ring ?x_22 ?x_23 [class_instances] (1) ?x_23 : normed_ring ℂ := @normed_field.to_normed_ring ?x_24 ?x_25 [class_instances] (2) ?x_25 : normed_field ℂ := complex.normed_field [class_instances] (1) ?x_15 : comm_ring ?x_14 := @subalgebra.comm_ring ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 [class_instances] (2) ?x_29 : comm_ring ?x_27 := @subalgebra.comm_ring ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 [class_instances] (3) ?x_35 : comm_ring ?x_33 := @subalgebra.comm_ring ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43 [class_instances] (4) ?x_41 : comm_ring ?x_39 := @subalgebra.comm_ring ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49 [class_instances] (5) ?x_47 : comm_ring ?x_45 := @subalgebra.comm_ring ?x_50 ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 [class_instances] (6) ?x_53 : comm_ring ?x_51 := @subalgebra.comm_ring ?x_56 ?x_57 ?x_58 ?x_59 ?x_60 ?x_61 [class_instances] (7) ?x_59 : comm_ring ?x_57 := @subalgebra.comm_ring ?x_62 ?x_63 ?x_64 ?x_65 ?x_66 ?x_67 [class_instances] (8) ?x_65 : comm_ring ?x_63 := @subalgebra.comm_ring ?x_68 ?x_69 ?x_70 ?x_71 ?x_72 ?x_73 [class_instances] (9) ?x_71 : comm_ring ?x_69 := @subalgebra.comm_ring ?x_74 ?x_75 ?x_76 ?x_77 ?x_78 ?x_79 [class_instances] (10) ?x_77 : comm_ring ?x_75 := @subalgebra.comm_ring ?x_80 ?x_81 ?x_82 ?x_83 ?x_84 ?x_85 [class_instances] (11) ?x_83 : comm_ring ?x_81 := @subalgebra.comm_ring ?x_86 ?x_87 ?x_88 ?x_89 ?x_90 ?x_91 [class_instances] (12) ?x_89 : comm_ring ?x_87 := @subalgebra.comm_ring ?x_92 ?x_93 ?x_94 ?x_95 ?x_96 ?x_97 [class_instances] (13) ?x_95 : comm_ring ?x_93 := @subalgebra.comm_ring ?x_98 ?x_99 ?x_100 ?x_101 ?x_102 ?x_103 [class_instances] (14) ?x_101 : comm_ring ?x_99 := @subalgebra.comm_ring ?x_104 ?x_105 ?x_106 ?x_107 ?x_108 ?x_109 [class_instances] (15) ?x_107 : comm_ring ?x_105 := @subalgebra.comm_ring ?x_110 ?x_111 ?x_112 ?x_113 ?x_114 ?x_115 [class_instances] (16) ?x_113 : comm_ring ?x_111 := @subalgebra.comm_ring ?x_116 ?x_117 ?x_118 ?x_119 ?x_120 ?x_121 [class_instances] (17) ?x_119 : comm_ring ?x_117 := @subalgebra.comm_ring ?x_122 ?x_123 ?x_124 ?x_125 ?x_126 ?x_127 [class_instances] (18) ?x_125 : comm_ring ?x_123 := @subalgebra.comm_ring ?x_128 ?x_129 ?x_130 ?x_131 ?x_132 ?x_133 [class_instances] (19) ?x_131 : comm_ring ?x_129 := @subalgebra.comm_ring ?x_134 ?x_135 ?x_136 ?x_137 ?x_138 ?x_139 [class_instances] (20) ?x_1

[Floris van Doorn]

The problem here is that comm_ring ?x_14 tries to find a class on a (meta)variable type, which typically means that all instances match.
What is the last instance step in the trace without metavariables yet? That instance is likely the culprit.

[Chris Hughes]

I think it's something to do with normed_ring. I think I remember Mario saying that that was theoretically bad even though it hadn't caused problems yet.

[Chris Hughes]

I see the problem now I think. My bad, there's an unused argument in algebra.vector_space