From 6e6609f2aaf412face8f4e5e18c139b51a9984cb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 26 Sep 2016 16:44:29 -0700
Subject: [PATCH] fix(frontends/lean): use coercions to sort at elaborate_type

---
 src/frontends/lean/elaborator.cpp            |  7 ++++---
 tests/lean/run/coe_univ_bug.lean             | 13 +++++++++++++
 tests/lean/run/pred_to_subtype_coercion.lean |  3 +++
 3 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 5fa216dd2e..6f63f52fc2 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2455,9 +2455,10 @@ expr elaborator::elaborate(expr const & e) {
 }
 
 expr elaborator::elaborate_type(expr const & e) {
-    expr Type  = copy_tag(e, mk_sort(mk_level_placeholder()));
-    expr new_e = copy_tag(e, mk_typed_expr(Type, e));
-    return elaborate(e);
+    expr const & ref = e;
+    expr new_e = ensure_type(visit(e, none_expr()), ref);
+    synthesize();
+    return new_e;
 }
 
 expr_pair elaborator::elaborate_with_type(expr const & e, expr const & e_type) {
diff --git a/tests/lean/run/coe_univ_bug.lean b/tests/lean/run/coe_univ_bug.lean
index 9a8233a082..60aa0e52ad 100644
--- a/tests/lean/run/coe_univ_bug.lean
+++ b/tests/lean/run/coe_univ_bug.lean
@@ -5,3 +5,16 @@ def below (n : nat) : nat → Prop :=
 
 def f {n : nat} (v : subtype (below n)) : nat :=
 v + 1
+
+universe variable u
+
+instance pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
+⟨Type (max 1 u), (λ p : A → Prop, subtype p)⟩
+
+instance coesubtype {A : Type u} {p : A → Prop} : has_coe (@coe_sort _ pred2subtype p) A :=
+⟨λ s, subtype.elt_of s⟩
+
+def g {n : nat} (v : below n) : nat :=
+v + 1
+
+print g
diff --git a/tests/lean/run/pred_to_subtype_coercion.lean b/tests/lean/run/pred_to_subtype_coercion.lean
index 9d4f80676b..d1c560240f 100644
--- a/tests/lean/run/pred_to_subtype_coercion.lean
+++ b/tests/lean/run/pred_to_subtype_coercion.lean
@@ -16,3 +16,6 @@ lemma zlt10 : 0 < 10 :=
 sorry
 
 check f ⟨0, zlt10⟩
+
+definition g (a : below 10) : nat :=
+subtype.elt_of a