fix(frontends/lean): alias generation for composite names was not working

This is an issue for declarations that generate composite names such as
the inductive datatype packacke.

The commit also fix a bug in the generate of aliases for recursors

src/frontends/lean/inductive_cmd.cpp

@@ -571,19 +571,29 @@ struct inductive_cmd_fn {
         }
     }
 
+    /** \brief Return true if eliminator/recursor can eliminate into any universe */
+    bool has_general_eliminator(environment const & env, name const & d_name) {
+        declaration d = env.get(d_name);
+        declaration r = env.get(mk_rec_name(d_name));
+        return length(d.get_univ_params()) != length(r.get_univ_params());
+    }
+
     /** \brief Add aliases for the inductive datatype, introduction and elimination rules */
     environment add_aliases(environment env, level_param_names const & ls, buffer<expr> const & locals,
                             buffer<inductive_decl> const & decls) {
         buffer<expr> params_only(locals);
         remove_local_vars(m_p, params_only);
         // Create aliases/local refs
-        levels ctx_levels = collect_local_nonvar_levels(m_p, ls);
+        levels ctx_levels     = collect_local_nonvar_levels(m_p, ls);
         for (auto & d : decls) {
             name d_name = inductive_decl_name(d);
             name d_short_name(d_name.get_string());
             env = add_alias(m_p, env, false, d_name, ctx_levels, params_only);
             name rec_name = mk_rec_name(d_name);
-            env = add_alias(m_p, env, true, rec_name, ctx_levels, params_only);
+            levels rec_ctx_levels = ctx_levels;
+            if (ctx_levels && has_general_eliminator(env, d_name))
+                rec_ctx_levels = levels(mk_level_placeholder(), rec_ctx_levels);
+            env = add_alias(m_p, env, true, rec_name, rec_ctx_levels, params_only);
             env = add_protected(env, rec_name);
             for (intro_rule const & ir : inductive_decl_intros(d)) {
                 name ir_name = intro_rule_name(ir);

src/frontends/lean/parser.cpp

@@ -1033,14 +1033,12 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
         ls = to_list(lvl_buffer.begin(), lvl_buffer.end());
     }
 
-    if (id.is_atomic()) {
+    // locals
-        // locals
+    if (auto it1 = m_local_decls.find(id)) {
-        if (auto it1 = m_local_decls.find(id)) {
+        auto r = copy_with_new_pos(propagate_levels(*it1, ls), p);
-            auto r = copy_with_new_pos(propagate_levels(*it1, ls), p);
+        save_type_info(r);
-            save_type_info(r);
+        save_identifier_info(p, id);
-            save_identifier_info(p, id);
+        return r;
-            return r;
-        }
     }
 
     for (name const & ns : get_namespaces(m_env)) {

src/frontends/lean/util.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "library/locals.h"
 #include "library/explicit.h"
+#include "library/placeholder.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 
@@ -150,7 +151,7 @@ expr update_local_ref(expr const & e, name_set const & lvls_to_remove, name_set
         expr const & c = get_explicit_arg(f);
         lean_assert(is_constant(c));
         new_f = mk_explicit(update_constant(c, filter(const_levels(c), [&](level const & l) {
-                        return is_param(l) && !lvls_to_remove.contains(param_id(l));
+                        return is_placeholder(l) || (is_param(l) && !lvls_to_remove.contains(param_id(l)));
                     })));
     } else {
         new_f = f;

tests/lean/run/section4.lean

@@ -1,5 +1,8 @@
 import logic
 
+  set_option pp.universes true
+  set_option pp.implicit true
+
 context
   universe k
   parameter A : Type
@@ -12,7 +15,13 @@ context
 
     inductive mypair :=
     mk : A → B → mypair
+
+    definition pr1' (p : mypair) : A := mypair.rec (λ a b, a) p
+    definition pr2' (p : mypair) : B := mypair.rec (λ a b, b) p
+    check mypair.rec
+
   end
+  check mypair.rec
   variable a : A
   check foo num a 0
   definition pr1 (p : mypair num) : A   := mypair.rec (λ a b, a) p