Relax definition of identity_stack. Fix printer for metavariable contexts.

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

src/kernel/normalizer.cpp

@@ -144,8 +144,6 @@ class normalizer::imp {
 
     /** \brief Return true iff the value_stack does affect the context of a metavariable */
     bool is_identity_stack(value_stack const & s, unsigned k) {
-        if (length(s) != k)
-            return false;
         unsigned i = 0;
         for (auto e : s) {
             if (e.kind() != svalue_kind::BoundedVar || k - to_bvar(e) - 1 != i)

src/library/printer.cpp

@@ -87,7 +87,7 @@ struct print_expr_fn {
                 } else {
                     lean_assert(e.is_inst());
                     out() << "inst:" << e.s() << " ";
-                    print_child(e.v(), c);
+                    print_child(e.v(), context());
                 }
             }
             out() << "]";

src/tests/kernel/metavar.cpp

@@ -392,6 +392,22 @@ static void tst18() {
                 Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z))));
 }
 
+static void tst19() {
+    environment env;
+    metavar_env menv;
+    normalizer  norm(env);
+    context ctx;
+    ctx = extend(ctx, "w1", Type());
+    ctx = extend(ctx, "w2", Type());
+    expr m1 = menv.mk_metavar();
+    expr x = Const("x");
+    expr y = Const("y");
+    expr N = Const("N");
+    expr F = Fun({{N, Type()}, {x, N}, {y, N}}, m1);
+    std::cout << norm(F) << "\n";
+    std::cout << norm(F, ctx) << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -411,5 +427,6 @@ int main() {
     tst16();
     tst17();
     tst18();
+    tst19();
     return has_violations() ? 1 : 0;
 }