refactor(library/init/core): simpler has_insert type class with out_param

library/init/core.lean

@@ -252,7 +252,7 @@ class has_ssubset  (α : Type u) := (ssubset : α → α → Prop)
    used to implement polymorphic notation for collections.
    Example: {a, b, c}. -/
 class has_emptyc   (α : Type u) := (emptyc : α)
-class has_insert   (α : Type u) (γ : Type u → Type v) := (insert : α → γ α → γ α)
+class has_insert   (α : out_param (Type u)) (γ : Type v) := (insert : α → γ → γ)
 /- Type class used to implement the notation { a ∈ c | p a } -/
 class has_sep (α : Type u) (γ : Type u → Type v) :=
 (sep : (α → Prop) → γ α → γ α)
@@ -291,14 +291,14 @@ def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α :=
 
 attribute [pattern] zero one bit0 bit1 add neg
 
-def insert {α : Type u} {γ : Type u → Type v} [has_insert α γ] : α → γ α → γ α :=
+def insert {α : Type u} {γ : Type v} [has_insert α γ] : α → γ → γ :=
 has_insert.insert
 
 /- The empty collection -/
 def emptyc {α : Type u} [has_emptyc α] : α :=
 has_emptyc.emptyc α
 
-def singleton {α : Type u} {γ : Type u → Type v} [has_emptyc (γ α)] [has_insert α γ] (a : α) : γ α :=
+def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ :=
 insert a emptyc
 
 def sep {α : Type u} {γ : Type u → Type v} [has_sep α γ] : (α → Prop) → γ α → γ α :=

library/init/data/list/basic.lean

@@ -51,7 +51,7 @@ instance : has_emptyc (list α) :=
 protected def insert [decidable_eq α] (a : α) (l : list α) : list α :=
 if a ∈ l then l else concat l a
 
-instance [decidable_eq α] : has_insert α list :=
+instance [decidable_eq α] : has_insert α (list α) :=
 ⟨list.insert⟩
 
 protected def union [decidable_eq α] : list α → list α → list α

library/init/data/set.lean

@@ -39,7 +39,7 @@ instance : has_emptyc (set α) :=
 protected def insert (a : α) (s : set α) : set α :=
 {b | b = a ∨ b ∈ s}
 
-instance : has_insert α set :=
+instance : has_insert α (set α) :=
 ⟨set.insert⟩
 
 protected def union (s₁ s₂ : set α) : set α :=

tests/lean/emptyc_errors.lean.expected.out

@@ -2,10 +2,10 @@ emptyc_errors.lean:4:52: error: don't know how to synthesize placeholder
 context:
 A : Type u,
 x : A
-⊢ Type u → Type ?
+⊢ has_mem A ?m_1
 emptyc_errors.lean:4:52: error: don't know how to synthesize placeholder
 context:
 A : Type u,
 x : A
-⊢ Type u → Type ?
+⊢ has_mem A ?m_1
 emptyc_errors.lean:4:52: error: elaborator failed

tests/lean/run/mem_nil.lean

@@ -1,4 +1,4 @@
 universe variables u
 
-example {α : Type u} (a : α) : a ∉ [] :=
+example {α : Type u} (a : α) : a ∉ ([] : list α) :=
 sorry

tests/lean/struct_class.lean.expected.out

@@ -5,12 +5,12 @@ has_append : Type u → Type u
 has_div : Type u → Type u
 has_dvd : Type u → Type u
 has_emptyc : Type u → Type u
-has_insert : Type u → (Type u → Type v) → Type (max u v)
+has_insert : out_param Type u → Type v → Type (max u v)
 has_inter : Type u → Type u
 has_inv : Type u → Type u
 has_le : Type u → Type u
 has_lt : Type u → Type u
-has_mem : Type u → (Type u → Type v) → Type (max u v)
+has_mem : out_param Type u → Type v → Type (max u v)
 has_mod : Type u → Type u
 has_mul : Type u → Type u
 has_neg : Type u → Type u
@@ -31,12 +31,12 @@ has_append : Type u → Type u
 has_div : Type u → Type u
 has_dvd : Type u → Type u
 has_emptyc : Type u → Type u
-has_insert : Type u → (Type u → Type v) → Type (max u v)
+has_insert : out_param Type u → Type v → Type (max u v)
 has_inter : Type u → Type u
 has_inv : Type u → Type u
 has_le : Type u → Type u
 has_lt : Type u → Type u
-has_mem : Type u → (Type u → Type v) → Type (max u v)
+has_mem : out_param Type u → Type v → Type (max u v)
 has_mod : Type u → Type u
 has_mul : Type u → Type u
 has_neg : Type u → Type u