fix(frontends/lean/parser): associated position with 'type' placeholder

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

src/frontends/lean/parser.cpp

@@ -721,7 +721,7 @@ class parser::imp {
             if (type)
                 arg_type = lift_free_vars(type, i);
             else
-                arg_type = mk_placholder();
+                arg_type = save(mk_placholder(), names[i].first);
             result[sz + i] = std::make_tuple(names[i].first, names[i].second, arg_type, implicit_decl);
         }
     }

src/library/elaborator/elaborator.cpp

@@ -269,7 +269,7 @@ class elaborator::imp {
     }
 
     /**
-       \brief Auxiliary method for pushing a new constraint to the given constraint queue.
+       \brief Push a new constraint to the given constraint queue.
        If \c is_eq is true, then a equality constraint is created, otherwise a convertability constraint is created.
     */
     void push_new_constraint(cnstr_queue & q, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
@@ -279,6 +279,10 @@ class elaborator::imp {
             q.push_front(mk_convertible_constraint(new_ctx, new_a, new_b, new_jst));
     }
 
+    /**
+       \brief Push a new equality constraint <tt>new_ctx |- new_a == new_b</tt> into the given contraint queue using
+       justification \c new_jst.
+    */
     void push_new_eq_constraint(cnstr_queue & q, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
         push_new_constraint(q, true, new_ctx, new_a, new_b, new_jst);
     }

tests/lean/ty1.lean

@@ -0,0 +1,8 @@
+Variable i : Int.
+Check fun x, x + i
+Check fun x, x + 1
+Check fun x, x
+Check fun x y, y + i + 1 + x
+Check (fun x, x) i
+Check (fun x, x i) (fun x y, x + 1 + y)
+Check (fun x, x) (fun x y, x + 1 + y)

tests/lean/ty1.lean.expected.out

@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: i
+λ x : ℤ, x + i : ℤ → ℤ
+λ x : ℕ, x + 1 : ℕ → ℕ
+Error (line: 4, pos: 10) unexpected metavariable occurrence
+λ x y : ℤ, y + i + 1 + x : ℤ → ℤ → ℤ
+(λ x : ℤ, x) i : ℤ
+(λ x : ℤ → ℤ → ℤ, x i) (λ x y : ℤ, x + 1 + y) : ℤ → ℤ
+(λ x : ℕ → ℕ → ℕ, x) (λ x y : ℕ, x + 1 + y) : ℕ → ℕ → ℕ