Commit 2021-10-13 15:48 9ee2a50a

fix(group_theory/group_action): has_scalar.comp.is_scalar_tower is a dangerous instance (#9656) This issue came up in the discussion of #9535: in certain cases, the instance has_scalar.comp.is_scalar_tower is fed too many metavariables and starts recursing infinitely. So I believe we should demote it from being an instance. Example trace:

[class_instances] (0) ?x_0 : has_scalar S P.quotient := @quotient.has_scalar ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
[class_instances] (1) ?x_9 : @is_scalar_tower S R M ?x_7
  (@smul_with_zero.to_has_scalar R M
     (@mul_zero_class.to_has_zero R
        (@mul_zero_one_class.to_mul_zero_class R
           (@monoid_with_zero.to_mul_zero_one_class R (@semiring.to_monoid_with_zero R (@ring.to_semiring R _inst_1)))))
     (@add_zero_class.to_has_zero M
        (@add_monoid.to_add_zero_class M
           (@add_comm_monoid.to_add_monoid M (@add_comm_group.to_add_comm_monoid M _inst_2))))
     (@mul_action_with_zero.to_smul_with_zero R M (@semiring.to_monoid_with_zero R (@ring.to_semiring R _inst_1))
        (@add_zero_class.to_has_zero M
           (@add_monoid.to_add_zero_class M
              (@add_comm_monoid.to_add_monoid M (@add_comm_group.to_add_comm_monoid M _inst_2))))
        (@module.to_mul_action_with_zero R M (@ring.to_semiring R _inst_1)
           (@add_comm_group.to_add_comm_monoid M _inst_2)
           _inst_3)))
  ?x_8 := @has_scalar.comp.is_scalar_tower ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19
[class_instances] (2) ?x_18 : @is_scalar_tower ?x_11 R M ?x_15
  (@smul_with_zero.to_has_scalar R M
     (@mul_zero_class.to_has_zero R
        (@mul_zero_one_class.to_mul_zero_class R
           (@monoid_with_zero.to_mul_zero_one_class R (@semiring.to_monoid_with_zero R (@ring.to_semiring R _inst_1)))))
     (@add_zero_class.to_has_zero M
        (@add_monoid.to_add_zero_class M
           (@add_comm_monoid.to_add_monoid M (@add_comm_group.to_add_comm_monoid M _inst_2))))
     (@mul_action_with_zero.to_smul_with_zero R M (@semiring.to_monoid_with_zero R (@ring.to_semiring R _inst_1))
        (@add_zero_class.to_has_zero M
           (@add_monoid.to_add_zero_class M
              (@add_comm_monoid.to_add_monoid M (@add_comm_group.to_add_comm_monoid M _inst_2))))
        (@module.to_mul_action_with_zero R M (@ring.to_semiring R _inst_1)
           (@add_comm_group.to_add_comm_monoid M _inst_2)
           _inst_3)))
  ?x_16 := @has_scalar.comp.is_scalar_tower ?x_20 ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28
...

You'll see that the places where has_scalar.comp.is_scalar_tower expects a has_scalar.comp are in fact metavariables, so they always unify. I have included a test case where the instance looks innocuous enough in its parameters: everything is phrased in terms of either irreducible defs, implicit variables or instance implicits, to argue that the issue really lies with has_scalar.comp.is_scalar_tower. Moreover, I don't think we lose a lot by demoting the latter from an instance since has_scalar.comp isn't an instance either.