feat(frontends/lean): use the same universe in declarations such as (A B : Type)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/elaborator.cpp

@@ -133,6 +133,8 @@ class elaborator {
     name_generator      m_ngen;
     type_checker_ptr    m_tc;
     substitution        m_subst;
+    expr_map<expr>      m_cache; // (pointer equality) cache for Type and Constants (this is a trick to make sure we get the
+                                 // same universe metavariable for different occurrences of the same Type/Constant
     context             m_ctx; // current local context: a list of local constants
     pos_info_provider * m_pos_provider; // optional expression position information used when reporting errors.
     justification       m_accumulated; // accumulate justification of eagerly used substitutions
@@ -713,7 +715,14 @@ public:
     }
 
     expr visit_sort(expr const & e) {
-        return update_sort(e, replace_univ_placeholder(sort_level(e)));
+        auto it = m_cache.find(e);
+        if (it != m_cache.end()) {
+            return it->second;
+        } else {
+            expr r = update_sort(e, replace_univ_placeholder(sort_level(e)));
+            m_cache.insert(mk_pair(e, r));
+            return r;
+        }
     }
 
     expr visit_macro(expr const & e) {
@@ -726,19 +735,26 @@ public:
     }
 
     expr visit_constant(expr const & e) {
-        declaration d = m_env.get(const_name(e));
+        auto it = m_cache.find(e);
-        buffer<level> ls;
+        if (it != m_cache.end()) {
-        for (level const & l : const_levels(e))
+            return it->second;
-            ls.push_back(replace_univ_placeholder(l));
+        } else {
-        unsigned num_univ_params = length(d.get_univ_params());
+            declaration d = m_env.get(const_name(e));
-        if (num_univ_params < ls.size())
+            buffer<level> ls;
-            throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #"
+            for (level const & l : const_levels(e))
-                                   << num_univ_params << " expected, #" << ls.size() << " provided");
+                ls.push_back(replace_univ_placeholder(l));
-        // "fill" with meta universe parameters
+            unsigned num_univ_params = length(d.get_univ_params());
-        for (unsigned i = ls.size(); i < num_univ_params; i++)
+            if (num_univ_params < ls.size())
-            ls.push_back(mk_meta_univ(m_ngen.next()));
+                throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #"
-        lean_assert(num_univ_params == ls.size());
+                                       << num_univ_params << " expected, #" << ls.size() << " provided");
-        return update_constant(e, to_list(ls.begin(), ls.end()));
+            // "fill" with meta universe parameters
+            for (unsigned i = ls.size(); i < num_univ_params; i++)
+                ls.push_back(mk_meta_univ(m_ngen.next()));
+            lean_assert(num_univ_params == ls.size());
+            expr r = update_constant(e, to_list(ls.begin(), ls.end()));
+            m_cache.insert(mk_pair(e, r));
+            return r;
+        }
     }
 
     /** \brief Make sure \c e is a type. If it is not, then try to apply coercions. */

tests/lean/run/tactic26.lean

@@ -1,7 +1,7 @@
 import standard
 using tactic
 
-inductive sum (A B : Type) : Type :=
+inductive sum (A : Type) (B : Type) : Type :=
 | inl  : A → sum A B
 | inr  : B → sum A B
 
@@ -19,4 +19,3 @@ definition my_tac := fixpoint (λ t, [ apply @inl_inhabited; t
 tactic_hint [inhabited] my_tac
 
 theorem T : inhabited (sum false num.num)
-

tests/lean/run/tactic28.lean

@@ -1,7 +1,7 @@
 import standard
 using tactic
 
-inductive sum (A B : Type) : Type :=
+inductive sum (A : Type) (B : Type) : Type :=
 | inl  : A → sum A B
 | inr  : B → sum A B