From 04a851810449cb79f0b8f063e64c7db2e7c2cc40 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Jan 2017 18:49:52 -0800
Subject: [PATCH] refactor(library/init/core): simpler has_insert type class
 with out_param

---
 library/init/core.lean                     | 6 +++---
 library/init/data/list/basic.lean          | 2 +-
 library/init/data/set.lean                 | 2 +-
 tests/lean/emptyc_errors.lean.expected.out | 4 ++--
 tests/lean/run/mem_nil.lean                | 2 +-
 tests/lean/struct_class.lean.expected.out  | 8 ++++----
 6 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/library/init/core.lean b/library/init/core.lean
index 7003244496..92952c544b 100644
--- a/library/init/core.lean
+++ b/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) → γ α → γ α :=
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index d722e0294a..a099c4e8fb 100644
--- a/library/init/data/list/basic.lean
+++ b/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 α
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index cfadbf276c..d445c885c1 100644
--- a/library/init/data/set.lean
+++ b/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 α :=
diff --git a/tests/lean/emptyc_errors.lean.expected.out b/tests/lean/emptyc_errors.lean.expected.out
index 8e785449de..fc99aabbe3 100644
--- a/tests/lean/emptyc_errors.lean.expected.out
+++ b/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
diff --git a/tests/lean/run/mem_nil.lean b/tests/lean/run/mem_nil.lean
index 9a4f50996a..2848d9581d 100644
--- a/tests/lean/run/mem_nil.lean
+++ b/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
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index 72ca0194cc..78577f9272 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/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