Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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: ```plain [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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
- Loading branch information