typeclass resolution failure

typeclass.txt

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) := @pi.semimodule ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) := @add_comm_monoid.nat_semimodule ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) := @semiring.to_semimodule ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) := @module.to_semimodule ?x_11 ?x_12 ?x_13 ?x_14 ?x_15
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_16 : ring α := _inst_1
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_17 : add_comm_group (β → α) := @pi.add_comm_group ?x_18 ?x_19 ?x_20
[class_instances] (1) ?x_20 i : add_comm_group α := @pi.add_comm_group (?x_21 i) (?x_22 i) (?x_23 i)
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := @submodule.add_comm_group (?x_24 i) (?x_25 i) (?x_26 i) (?x_27 i) (?x_28 i) (?x_29 i)
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := @subtype.add_comm_group (?x_30 i) (?x_31 i) (?x_32 i) _
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := rat.add_comm_group
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := @add_units.comm_group (?x_34 i) (?x_35 i)
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := @additive.add_comm_group (?x_36 i) (?x_37 i)
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := @prod.add_comm_group (?x_38 i) (?x_39 i) (?x_40 i) (?x_41 i)
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := @add_monoid_hom.add_comm_group (?x_42 i) (?x_43 i) (?x_44 i) (?x_45 i)
failed is_def_eq
[class_instances] (1) ?x_20 i : add_comm_group α := @nonneg_comm_group.to_add_comm_group (?x_46 i) (?x_47 i)
[class_instances] (2) ?x_47 i : nonneg_comm_group α := @linear_nonneg_ring.to_nonneg_comm_group (?x_48 i) (?x_49 i)
[class_instances] (2) ?x_47 i : nonneg_comm_group α := @nonneg_ring.to_nonneg_comm_group (?x_48 i) (?x_49 i)
[class_instances] (3) ?x_49 i : nonneg_ring α := @linear_nonneg_ring.to_nonneg_ring (?x_50 i) (?x_51 i)
[class_instances] (1) ?x_20 i : add_comm_group α := @ring.to_add_comm_group (?x_21 i) (?x_22 i)
[class_instances] (2) ?x_22 i : ring α := _inst_1
[class_instances] (1) ?x_15 : @module α (β → α) _inst_1
  (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1)) := @add_comm_group.int_module ?x_23 ?x_24
failed is_def_eq
[class_instances] (1) ?x_15 : @module α (β → α) _inst_1
  (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1)) := @subspace.vector_space ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30
failed is_def_eq
[class_instances] (1) ?x_15 : @module α (β → α) _inst_1
  (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1)) := @field.to_vector_space ?x_31 ?x_32
failed is_def_eq
[class_instances] (1) ?x_15 : @module α (β → α) _inst_1
  (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1)) := @submodule.module ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38
failed is_def_eq
[class_instances] (1) ?x_15 : @module α (β → α) _inst_1
  (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1)) := @ring.to_module ?x_39 ?x_40
failed is_def_eq