From 49a0d13c504c8dcaaeedb4312222d6e4c9a4e896 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 31 Jan 2017 16:53:04 -0800
Subject: [PATCH] feat(library/init/coe): add coercion from A to (option A)

A little hack is used to make sure type class resolution will not enter
in an infinite loop.
---
 library/init/coe.lean       | 45 +++++++++++++++++++++++++++++++------
 tests/lean/coe3.lean        |  1 +
 tests/lean/run/coe_opt.lean | 12 ++++++++++
 3 files changed, 51 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/coe_opt.lean

diff --git a/library/init/coe.lean b/library/init/coe.lean
index eaef675541..b0afde1b31 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -30,14 +30,14 @@ universe variables u v
 class has_lift (a : Sort u) (b : Sort v) :=
 (lift : a → b)
 
-/- auxiliary class that contains the transitive closure of has_lift. -/
+/- Auxiliary class that contains the transitive closure of has_lift. -/
 class has_lift_t (a : Sort u) (b : Sort v) :=
 (lift : a → b)
 
 class has_coe (a : Sort u) (b : Sort v) :=
 (coe : a → b)
 
-/- auxiliary class that contains the transitive closure of has_coe. -/
+/- Auxiliary class that contains the transitive closure of has_coe. -/
 class has_coe_t (a : Sort u) (b : Sort v) :=
 (coe : a → b)
 
@@ -97,13 +97,44 @@ instance coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe a b]
 instance coe_base {a : Sort u} {b : Sort v} [has_coe a b] : has_coe_t a b :=
 ⟨coe_b⟩
 
-instance coe_fn_trans {a : Sort u₁} {b : Sort u₂} [has_lift_t a b] [has_coe_to_fun.{u₂ u₃} b] : has_coe_to_fun.{u₁ u₃} a :=
-{ F   := λ x, @has_coe_to_fun.F.{u₂ u₃} b _ (coe x),
-  coe := λ x, coe_fn (coe x) }
+/- We add this instance directly into has_coe_t to avoid non-termination.
 
-instance coe_sort_trans {a : Sort u₁} {b : Sort u₂} [has_lift_t a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a :=
+   Suppose coe_option had type (has_coe a (option a)).
+   Then, we can loop when searching a coercion from α to β (has_coe_t α β)
+   1- coe_trans at (has_coe_t α β)
+          (has_coe α ?b₁) and (has_coe_t ?b₁ c)
+   2- coe_option at (has_coe α ?b₁)
+          ?b₁ := option α
+   3- coe_trans at (has_coe_t (option α) β)
+          (has_coe (option α) ?b₂) and (has_coe_t ?b₂ β)
+   4- coe_option at (has_coe (option α) ?b₂)
+          ?b₂ := option (option α))
+   ...
+-/
+instance coe_option {a : Type u} : has_coe_t a (option a) :=
+⟨λ x, some x⟩
+
+/- Auxiliary transitive closure for has_coe which does not contain
+   instances such as coe_option.
+
+   They would produce non-termination when combined with coe_fn_trans and coe_sort_trans.
+-/
+class has_coe_t_aux (a : Sort u) (b : Sort v) :=
+(coe : a → b)
+
+instance coe_trans_aux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe a b] [has_coe_t_aux b c] : has_coe_t_aux a c :=
+⟨λ x : a, @has_coe_t_aux.coe b c _ (coe_b x)⟩
+
+instance coe_base_aux {a : Sort u} {b : Sort v} [has_coe a b] : has_coe_t_aux a b :=
+⟨coe_b⟩
+
+instance coe_fn_trans {a : Sort u₁} {b : Sort u₂} [has_coe_t_aux a b] [has_coe_to_fun.{u₂ u₃} b] : has_coe_to_fun.{u₁ u₃} a :=
+{ F   := λ x, @has_coe_to_fun.F.{u₂ u₃} b _ (@has_coe_t_aux.coe a b _ x),
+  coe := λ x, coe_fn (@has_coe_t_aux.coe a b _ x) }
+
+instance coe_sort_trans {a : Sort u₁} {b : Sort u₂} [has_coe_t_aux a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a :=
 { S   := has_coe_to_sort.S.{u₂ u₃} b,
-  coe := λ x, coe_sort (coe x) }
+  coe := λ x, coe_sort (@has_coe_t_aux.coe a b _ x) }
 
 /- Every coercion is also a lift -/
 
diff --git a/tests/lean/coe3.lean b/tests/lean/coe3.lean
index 700f0d2513..b43a217e0d 100644
--- a/tests/lean/coe3.lean
+++ b/tests/lean/coe3.lean
@@ -12,4 +12,5 @@ constant f : C → C
 constant g : D → D
 
 check f a
+
 check g a
diff --git a/tests/lean/run/coe_opt.lean b/tests/lean/run/coe_opt.lean
new file mode 100644
index 0000000000..d424563b62
--- /dev/null
+++ b/tests/lean/run/coe_opt.lean
@@ -0,0 +1,12 @@
+def f : nat → option nat → nat
+| a none     := a
+| a (some b) := a + b
+
+example (a b : nat) : f a b = a + b :=
+rfl
+
+example (a b : nat) : f a b = f a (some b) :=
+rfl
+
+example : f 1 (1:nat) = 2 :=
+rfl