fix(group_theory/group_action): has_scalar.comp.is_scalar_tower is a dangerous instance (#9656)

Vierkantor · Vierkantor · commit 9ee2a50aa439 · 2021-10-13T15:48:22.000Z
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>
diff --git a/src/group_theory/group_action/defs.lean b/src/group_theory/group_action/defs.lean
@@ -173,9 +173,15 @@ def comp (g : N → M) : has_scalar N α :=
 
 variables {α}
 
-/-- If an action forms a scalar tower then so does the action formed by `has_scalar.comp`. -/
+/-- Given a tower of scalar actions `M → α → β`, if we use `has_scalar.comp`
+to pull back both of `M`'s actions by a map `g : N → M`, then we obtain a new
+tower of scalar actions `N → α → β`.
+
+This cannot be an instance because it can cause infinite loops whenever the `has_scalar` arguments
+are still metavariables.
+-/
 @[priority 100]
-instance comp.is_scalar_tower [has_scalar M β] [has_scalar α β] [is_scalar_tower M α β]
+lemma comp.is_scalar_tower [has_scalar M β] [has_scalar α β] [is_scalar_tower M α β]
   (g : N → M) :
   (by haveI := comp α g; haveI := comp β g; exact is_scalar_tower N α β) :=
 by exact {smul_assoc := λ n, @smul_assoc _ _ _ _ _ _ _ (g n) }
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
@@ -281,6 +281,8 @@ variables {R' : Type*} [semiring R'] [module R' M] (f : R ≃+* R') (h : ∀ c (
 
 include f h b
 
+local attribute [instance] has_scalar.comp.is_scalar_tower
+
 /-- If `R` and `R'` are isomorphic rings that act identically on a module `M`,
 then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.
 
diff --git a/test/has_scalar_comp_loop.lean b/test/has_scalar_comp_loop.lean
@@ -0,0 +1,39 @@
+import group_theory.group_action.basic
+
+variables (R M S : Type*)
+
+/-- Some arbitrary type depending on `has_scalar R M` -/
+@[irreducible, nolint has_inhabited_instance unused_arguments]
+def foo [has_scalar R M] : Type* := ℕ
+
+variables [has_scalar R M] [has_scalar S R] [has_scalar S M]
+
+/-- This instance is incompatible with `has_scalar.comp.is_scalar_tower`.
+However, all its parameters are (instance) implicits or irreducible defs, so it
+should not be dangerous. -/
+@[nolint unused_arguments]
+instance foo.has_scalar [is_scalar_tower S R M] : has_scalar S (foo R M) :=
+⟨λ _ _, by { unfold foo, exact 37 }⟩
+
+-- If there is no `is_scalar_tower S R M` parameter, this should fail quickly,
+-- not loop forever.
+example : has_scalar S (foo R M) :=
+begin
+  tactic.success_if_fail_with_msg tactic.interactive.apply_instance
+    "tactic.mk_instance failed to generate instance for
+  has_scalar S (foo R M)",
+  unfold foo,
+  exact ⟨λ _ _, 37⟩
+end
+
+/-
+local attribute [instance] has_scalar.comp.is_scalar_tower
+-- When `has_scalar.comp.is_scalar_tower` is an instance, this recurses indefinitely.
+example : has_scalar S (foo R M) :=
+begin
+  tactic.success_if_fail_with_msg tactic.interactive.apply_instance
+    "maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')",
+  unfold foo,
+  exact ⟨λ _ _, 37⟩
+end
+-/
