Zulip Chat Archive

Stream: maths

Topic: subalgebra.comm_ring


view this post on Zulip Chris Hughes (Oct 11 2019 at 00:07):

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

view this post on Zulip Chris Hughes (Oct 11 2019 at 00:10):

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

view this post on Zulip Floris van Doorn (Oct 11 2019 at 00:10):

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.

view this post on Zulip Chris Hughes (Oct 11 2019 at 00:11):

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.

view this post on Zulip Chris Hughes (Oct 11 2019 at 00:14):

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


Last updated: May 19 2021 at 02:10 UTC