From 9c55bbb8717c8d7d0dbf677334e6fd6a0074717f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 29 Sep 2014 08:18:10 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): report an error when Type
 becomes a Prop after elaboration, closes #208

---
 library/algebra/relation.lean     |  4 ++--
 src/frontends/lean/elaborator.cpp | 36 +++++++++++++++++++++++++++++--
 tests/lean/run/elab_bug1.lean     |  2 +-
 3 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean
index 81d6717d0..1810fdb90 100644
--- a/library/algebra/relation.lean
+++ b/library/algebra/relation.lean
@@ -161,12 +161,12 @@ congruence.mk (λx y H, H)
 -- Relations that can be coerced to functions / implications
 -- ---------------------------------------------------------
 
-inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop :=
+inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
 mk {} : (a → b) → @mp_like R a b H
 
 namespace mp_like
 
-  definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
+  definition app.{l} {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
     (C : mp_like H) : a → b := rec (λx, x) C
 
   definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 99ce13e31..d17b75c9b 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -75,7 +75,7 @@ typedef name_map<expr> mvar2meta;
 class elaborator : public coercion_info_manager {
     typedef name_map<expr> local_tactic_hints;
     typedef rb_map<expr, pair<expr, constraint_seq>, expr_quick_cmp> cache;
-
+    typedef std::vector<pair<expr, expr>> to_check_sorts;
     elaborator_context & m_env;
     name_generator       m_ngen;
     type_checker_ptr     m_tc[2];
@@ -85,6 +85,9 @@ class elaborator : public coercion_info_manager {
     local_context        m_full_context; // superset of m_context, it also contains non-contextual locals.
     mvar2meta            m_mvar2meta;
     cache                m_cache;
+    // The following vector contains sorts that we should check
+    // whether the computed universe is too specific or not.
+    to_check_sorts       m_to_check_sorts;
 
     // mapping from metavariable name ?m to tactic expression that should be used to solve it.
     // this mapping is populated by the 'by tactic-expr' expression.
@@ -598,7 +601,10 @@ public:
     }
 
     expr visit_sort(expr const & e) {
-        return update_sort(e, replace_univ_placeholder(sort_level(e)));
+        expr r = update_sort(e, replace_univ_placeholder(sort_level(e)));
+        if (is_placeholder(sort_level(e)))
+            m_to_check_sorts.emplace_back(e, r);
+        return r;
     }
 
     expr visit_macro(expr const & e, constraint_seq & cs) {
@@ -984,6 +990,30 @@ public:
         }
     }
 
+    /** \brief Check whether the solution found by the elaborator is producing too specific
+        universes.
+
+        \remark For now, we only check if a term Type.{?u} was solved by assigning ?u to 0.
+        In this case, the user should write Prop instead of Type.
+    */
+    void check_sort_assignments(substitution const & s) {
+        for (auto const & p : m_to_check_sorts) {
+            expr pre  = p.first;
+            expr post = p.second;
+            lean_assert(is_sort(post));
+            level u   = sort_level(post);
+            lean_assert(is_meta(u));
+            if (s.is_assigned(u)) {
+                level r = *s.get_level(u);
+                if (is_zero(r)) {
+                    throw_kernel_exception(env(), pre, [=](formatter const &) {
+                            return format("solution computed by the elaborator forces Type to be Prop");
+                        });
+                }
+            }
+        }
+    }
+
     /** \brief Apply substitution and solve remaining metavariables using tactics. */
     expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params) {
         expr r = s.instantiate(e);
@@ -1013,6 +1043,7 @@ public:
         auto p  = solve(cs).pull();
         lean_assert(p);
         substitution s = p->first.first;
+        check_sort_assignments(s);
         auto result = apply(s, r);
         copy_info_to_manager(s);
         return result;
@@ -1038,6 +1069,7 @@ public:
         auto p  = solve(cs).pull();
         lean_assert(p);
         substitution s = p->first.first;
+        check_sort_assignments(s);
         name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t));
         buffer<name> new_params;
         expr new_r_t = apply(s, r_t, univ_params, new_params);
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index d145f1757..b571e9b10 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -11,7 +11,7 @@ open function
 namespace congruence
 
 -- TODO: move this somewhere else
-definition reflexive {T : Type} (R : T → T → Type) : Prop := ∀x, R x x
+definition reflexive {T : Type} (R : T → T → Prop) : Prop := ∀x, R x x
 
 -- Congruence classes for unary and binary functions
 -- -------------------------------------------------