From efd058459db95f057714db7fdaaf4526c136accb Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Wed, 25 Jan 2023 10:22:36 +0000
Subject: [PATCH] fix: Unbundled subclasses of `outParam` classes should not
 repeat the parents' `outParam`

This PR fixes a large amount of issues encountered in the port of `GroupTheory.Subgroup.Basic`, #1797. Subobject classes such as `MulMemClass` and `SubmonoidClass` take a `SetLike` parameter, and we were used to just copy over the `M : outParam Type` declaration from `SetLike`. Since Lean 3 synthesized from left to right, we'd fill in the `outParam` from `SetLike`, then the `Mul M` instance would be available for synthesis and we'd be in business. In Lean 4 however, we often go from right to left, so that `MulMemClass ?M S [?inst : Mul ?M]` is handled first, which can't be solved before finding a `Mul ?M` instance on the metavariable `?M`, causing search through all `Mul` instances.

The solution is: whenever a class is declared that takes another class as parameter (i.e. unbundled inheritance), the `outParam`s of the parent class should be unmarked and become in-params in the child class. Then Lean will try to find the parent class instance first, fill in the `outParam`s and we'll be able to synthesize the child class instance without problems.
---
 Mathlib/GroupTheory/Submonoid/Basic.lean    | 8 ++++----
 Mathlib/GroupTheory/Subsemigroup/Basic.lean | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/GroupTheory/Submonoid/Basic.lean b/Mathlib/GroupTheory/Submonoid/Basic.lean
index 03c0dec1f8ee0..f7c71a075abc1 100644
--- a/Mathlib/GroupTheory/Submonoid/Basic.lean
+++ b/Mathlib/GroupTheory/Submonoid/Basic.lean
@@ -72,7 +72,7 @@ variable [MulOneClass M] {s : Set M}
 variable [AddZeroClass A] {t : Set A}
 
 /-- `OneMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `1 ∈ s` for all `s`. -/
-class OneMemClass (S : Type _) (M : outParam <| Type _) [One M] [SetLike S M] : Prop where
+class OneMemClass (S : Type _) (M : Type _) [One M] [SetLike S M] : Prop where
   /-- By definition, if we have `OneMemClass S M`, we have `1 ∈ s` for all `s : S`. -/
   one_mem : ∀ s : S, (1 : M) ∈ s
 #align one_mem_class OneMemClass
@@ -80,7 +80,7 @@ class OneMemClass (S : Type _) (M : outParam <| Type _) [One M] [SetLike S M] :
 export OneMemClass (one_mem)
 
 /-- `ZeroMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`. -/
-class ZeroMemClass (S : Type _) (M : outParam <| Type _) [Zero M] [SetLike S M] : Prop where
+class ZeroMemClass (S : Type _) (M : Type _) [Zero M] [SetLike S M] : Prop where
   /-- By definition, if we have `ZeroMemClass S M`, we have `0 ∈ s` for all `s : S`. -/
   zero_mem : ∀ s : S, (0 : M) ∈ s
 #align zero_mem_class ZeroMemClass
@@ -104,7 +104,7 @@ add_decl_doc Submonoid.toSubsemigroup
 
 /-- `SubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `1`
 and are closed under `(*)` -/
-class SubmonoidClass (S : Type _) (M : outParam <| Type _) [MulOneClass M] [SetLike S M] extends
+class SubmonoidClass (S : Type _) (M : Type _) [MulOneClass M] [SetLike S M] extends
   MulMemClass S M, OneMemClass S M : Prop
 #align submonoid_class SubmonoidClass
 
@@ -125,7 +125,7 @@ add_decl_doc AddSubmonoid.toAddSubsemigroup
 
 /-- `AddSubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `0`
 and are closed under `(+)` -/
-class AddSubmonoidClass (S : Type _) (M : outParam <| Type _) [AddZeroClass M] [SetLike S M] extends
+class AddSubmonoidClass (S : Type _) (M : Type _) [AddZeroClass M] [SetLike S M] extends
   AddMemClass S M, ZeroMemClass S M : Prop
 #align add_submonoid_class AddSubmonoidClass
 
diff --git a/Mathlib/GroupTheory/Subsemigroup/Basic.lean b/Mathlib/GroupTheory/Subsemigroup/Basic.lean
index 4a7c7974f447f..f6e09555a74fa 100644
--- a/Mathlib/GroupTheory/Subsemigroup/Basic.lean
+++ b/Mathlib/GroupTheory/Subsemigroup/Basic.lean
@@ -62,7 +62,7 @@ variable [Mul M] {s : Set M}
 variable [Add A] {t : Set A}
 
 /-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)` -/
-class MulMemClass (S : Type _) (M : outParam <| Type _) [Mul M] [SetLike S M] : Prop where
+class MulMemClass (S : Type _) (M : Type _) [Mul M] [SetLike S M] : Prop where
   /-- A substructure satisfying `MulMemClass` is closed under multiplication. -/
   mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
 #align mul_mem_class MulMemClass
@@ -70,7 +70,7 @@ class MulMemClass (S : Type _) (M : outParam <| Type _) [Mul M] [SetLike S M] :
 export MulMemClass (mul_mem)
 
 /-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)` -/
-class AddMemClass (S : Type _) (M : outParam <| Type _) [Add M] [SetLike S M] : Prop where
+class AddMemClass (S : Type _) (M : Type _) [Add M] [SetLike S M] : Prop where
   /-- A substructure satisfying `AddMemClass` is closed under addition. -/
   add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s
 #align add_mem_class AddMemClass