fix: Unbundled subclasses of outParam classes should not repeat the…

… parents' `outParam` (#1832)

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.

Pair: leanprover-community/mathlib#18291

Mathlib/Data/SetLike/Basic.lean

@@ -84,6 +84,15 @@ Note: if `SetLike.coe` is a projection, implementers should create a simp lemma
 @[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl
 ```
 to normalize terms.
+
+If you declare an unbundled subclass of `SetLike`, for example:
+```
+class MulMemClass (S : Type _) (M : Type _) [Mul M] [SetLike S M] where
+  ...
+```
+Then you should *not* repeat the `outParam` declaration so `SetLike` will supply the value instead.
+This ensures your subclass will not have issues with synthesis of the `[Mul M]` parameter starting
+before the value of `M` is known.
 -/
 class SetLike (A : Type _) (B : outParam <| Type _) where
   /-- The coercion from a term of a `SetLike` to its corresponding `Set`. -/

Mathlib/GroupTheory/Submonoid/Basic.lean

@@ -72,15 +72,15 @@ 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
 
 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
 

Mathlib/GroupTheory/Subsemigroup/Basic.lean

@@ -62,15 +62,15 @@ 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
 
 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