Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception.

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

src/frontends/lean/lean_elaborator.cpp

@@ -262,7 +262,7 @@ class elaborator::imp {
                     if (!has_metavar(expected) && !has_metavar(given)) {
                         if (is_convertible(expected, given, ctx)) {
                             // compatible
-                        } else if (m_frontend.get_coercion(given, expected)) {
+                        } else if (m_frontend.get_coercion(given, expected, ctx)) {
                             // compatible if using coercion
                             num_coercions++;
                         } else {
@@ -381,7 +381,7 @@ class elaborator::imp {
                         m_constraints.push_back(constraint(expected, given, ctx, r));
                     } else {
                         if (!is_convertible(expected, given, ctx)) {
-                            expr coercion = m_frontend.get_coercion(given, expected);
+                            expr coercion = m_frontend.get_coercion(given, expected, ctx);
                             if (coercion) {
                                 modified = true;
                                 args[i] = mk_app(coercion, args[i]);
@@ -437,7 +437,7 @@ class elaborator::imp {
                     m_constraints.push_back(constraint(expected, given, ctx, r));
                 } else {
                     if (!is_convertible(expected, given, ctx)) {
-                        expr coercion = m_frontend.get_coercion(given, expected);
+                        expr coercion = m_frontend.get_coercion(given, expected, ctx);
                         if (coercion) {
                             v_p.first = mk_app(coercion, v_p.first);
                         } else {
@@ -447,7 +447,7 @@ class elaborator::imp {
                 }
             }
             auto b_p = process(let_body(e), extend(ctx, let_name(e), t_p.first ? t_p.first : v_p.second, v_p.first));
-            expr t   = lower_free_vars_mmv(b_p.second, 1, 1);
+            expr t   = instantiate_free_var_mmv(b_p.second, 0, v_p.first);
             expr new_e = update_let(e, t_p.first, v_p.first, b_p.first);
             add_trace(e, new_e);
             return expr_pair(new_e, t);

src/frontends/lean/lean_frontend.cpp

@@ -324,9 +324,9 @@ struct frontend::imp {
             return expr();
     }
 
-    expr get_coercion(expr const & given_type, expr const & expected_type) {
+    expr get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) {
-        expr norm_given_type    = m_env.normalize(given_type);
+        expr norm_given_type    = m_env.normalize(given_type, ctx);
-        expr norm_expected_type = m_env.normalize(expected_type);
+        expr norm_expected_type = m_env.normalize(expected_type, ctx);
         return get_coercion_core(norm_given_type, norm_expected_type);
     }
 
@@ -414,7 +414,9 @@ std::vector<bool> const & frontend::get_implicit_arguments(name const & n) const
 name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); }
 
 void frontend::add_coercion(expr const & f) { m_imp->add_coercion(f); }
-expr frontend::get_coercion(expr const & given_type, expr const & expected_type) const { return m_imp->get_coercion(given_type, expected_type); }
+expr frontend::get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) const {
+    return m_imp->get_coercion(given_type, expected_type, ctx);
+}
 bool frontend::is_coercion(expr const & f) const { return m_imp->is_coercion(f); }
 
 state const & frontend::get_state() const { return m_imp->m_state; }

src/frontends/lean/lean_frontend.h

@@ -168,7 +168,7 @@ public:
         Return the null expression if there is no coercion from \c given_type to
         \c expected_type.
     */
-    expr get_coercion(expr const & given_type, expr const & expected_type) const;
+    expr get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) const;
     /**
        \brief Return true iff the given expression is a coercion. That is, it was added using
        \c add_coercion.

src/kernel/kernel_exception.h

@@ -175,6 +175,7 @@ public:
     expr const & get_type() const { return m_type; }
     expr const & get_value() const { return m_value; }
     expr const & get_value_type() const { return m_value_type; }
+    virtual expr const & get_main_expr() const { return m_value; }
     virtual char const * what() const noexcept { return "definition type mismatch"; }
 };
 

src/kernel/type_checker.cpp

@@ -140,7 +140,8 @@ public:
             }
             {
                 cache::mk_scope sc(m_cache);
-                r = lower_free_vars(infer_type(let_body(e), extend(ctx, let_name(e), lt, let_value(e))), 1);
+                expr t = infer_type(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
+                r = instantiate(t, let_value(e));
             }
             break;
         }

src/library/kernel_exception_formatter.cpp

@@ -88,14 +88,15 @@ format pp(formatter const & fmt, type_expected_exception const & ex, options con
 }
 
 format pp(formatter const & fmt, def_type_mismatch_exception const & ex, options const & opts) {
-    unsigned indent  = get_pp_indent(opts);
+    unsigned indent     = get_pp_indent(opts);
+    context const & ctx = ex.get_context();
     format r;
     r += format("type mismatch at definition '");
     r += format(ex.get_name());
     r += format("', expected type");
-    r += nest(indent, compose(line(), fmt(ex.get_type(), opts)));
+    r += nest(indent, compose(line(), fmt(ctx, ex.get_type(), false, opts)));
     r += compose(line(), format("Given type:"));
-    r += nest(indent, compose(line(), fmt(ex.get_value_type(), opts)));
+    r += nest(indent, compose(line(), fmt(ctx, ex.get_value_type(), false, opts)));
     return r;
 }
 

tests/lean/let4.lean

@@ -0,0 +1,51 @@
+
+Show
+let b := true,
+    a : Int := b
+in a
+
+Variable vector : Type -> Nat -> Type
+Variable const {A : Type} (n : Nat) (a : A) : vector A n
+
+Check
+let a  := 10,
+    v1 := const a true,
+    v2 := v1
+in v2
+
+Show
+let a  := 10,
+    v1 : vector Bool a := const a true,
+    v2 : vector Bool a := v1
+in v2
+
+Check
+let a  := 10,
+    v1 : vector Bool a := const a true,
+    v2 : vector Bool a := v1
+in v2
+
+Check
+let a  := 10,
+    v1 : vector Bool a := const a true,
+    v2 : vector Int  a := v1
+in v2
+
+Variable foo : (vector Bool 10) -> (vector Int 10)
+Coercion foo
+
+Check
+let a  := 10,
+    v1 : vector Bool a := const a true,
+    v2 : vector Int  a := v1
+in v2
+
+Set pp::coercion true
+
+Show
+let a  := 10,
+    v1 : vector Bool a := const a true,
+    v2 : vector Int  a := v1
+in v2
+
+

tests/lean/let4.lean.expected.out

@@ -0,0 +1,20 @@
+  Set: pp::colors
+  Set: pp::unicode
+Error (line: 4, pos: 15) type mismatch at definition 'a', expected type
+    ℤ
+Given type:
+    Bool
+  Assumed: vector
+  Assumed: const
+vector Bool 10
+let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2
+vector Bool 10
+Error (line: 31, pos: 26) type mismatch at definition 'v2', expected type
+    vector ℤ a
+Given type:
+    vector Bool a
+  Assumed: foo
+  Coercion foo
+vector ℤ 10
+  Set: lean::pp::coercion
+let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := foo v1 in v2