fix(frontends/lean/elaborator): class inference in tactic mode with trunc

closes #477

src/frontends/lean/elaborator.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/flycheck.h"
 #include "library/deep_copy.h"
 #include "library/typed_expr.h"
+#include "library/metavar_closure.h"
 #include "library/local_context.h"
 #include "library/constants.h"
 #include "library/util.h"
@@ -1905,8 +1906,11 @@ pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, opt
         }
     }
     expr e = translate(env(), ctx, n);
-    if (expected_type)
+    metavar_closure cls;
+    if (expected_type) {
         e = copy_tag(e, mk_typed_expr(mk_as_is(*expected_type), e));
+        cls.add(*expected_type);
+    }
     m_context.set_ctx(ctx);
     m_context.set_ctx(ctx);
     m_full_context.set_ctx(ctx);
@@ -1921,9 +1925,14 @@ pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, opt
     constraints rcs = p->first.second;
     r = s.instantiate_all(r);
     r = solve_unassigned_mvars(s, r);
+    rcs = map(rcs, [&](constraint const & c) { return instantiate_metavars(c, s); });
     copy_info_to_manager(s);
     if (report_unassigned)
         display_unassigned_mvars(r, s);
+    if (expected_type) {
+        justification j;
+        rcs = append(rcs, cls.mk_constraints(s, j, relax));
+    }
     return mk_pair(r, rcs);
 }
 

src/kernel/constraint.cpp

@@ -105,9 +105,12 @@ bool cnstr_on_demand(constraint const & c) {
     lean_assert(is_choice_cnstr(c));
     return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor.on_demand();
 }
-unsigned cnstr_delay_factor(constraint const & c) {
+delay_factor const & cnstr_delay_factor_core(constraint const & c) {
     lean_assert(is_choice_cnstr(c));
-    return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor.explict_value();
+    return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor;
+}
+unsigned cnstr_delay_factor(constraint const & c) {
+    return cnstr_delay_factor_core(c).explict_value();
 }
 bool cnstr_is_owner(constraint const & c) {
     lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_owner;

src/kernel/constraint.h

@@ -129,6 +129,7 @@ choice_fn const & cnstr_choice_fn(constraint const & c);
 /** \brief Return true iff the choice constraint should be solved as soon the type does not contains type variables */
 bool cnstr_on_demand(constraint const & c);
 /** \brief Return the choice constraint delay factor */
+delay_factor const & cnstr_delay_factor_core(constraint const & c);
 unsigned cnstr_delay_factor(constraint const & c);
 /** \brief Return true iff the given choice constraints owns the right to assign the metavariable in \c c. */
 bool cnstr_is_owner(constraint const & c);

src/library/util.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
+#include "kernel/metavar.h"
 #include "kernel/inductive/inductive.h"
 #include "library/locals.h"
 #include "library/util.h"
@@ -540,4 +541,29 @@ bool has_expr_metavar_relaxed(expr const & e) {
         });
     return found;
 }
+
+constraint instantiate_metavars(constraint const & c, substitution & s) {
+    switch (c.kind()) {
+    case constraint_kind::Eq:
+        return mk_eq_cnstr(s.instantiate_all(cnstr_lhs_expr(c)),
+                           s.instantiate_all(cnstr_rhs_expr(c)),
+                           c.get_justification(),
+                           relax_main_opaque(c));
+    case constraint_kind::LevelEq:
+        return mk_level_eq_cnstr(s.instantiate(cnstr_lhs_level(c)), s.instantiate(cnstr_rhs_level(c)), c.get_justification());
+    case constraint_kind::Choice: {
+        expr m = cnstr_expr(c);
+        lean_assert(is_meta(m));
+        buffer<expr> args;
+        expr mvar = get_app_args(m, args);
+        mvar = update_mlocal(mvar, s.instantiate_all(mlocal_type(mvar)));
+        for (expr & arg : args)
+            arg = s.instantiate_all(arg);
+        return mk_choice_cnstr(mk_app(mvar, args),
+                               cnstr_choice_fn(c),
+                               cnstr_delay_factor_core(c),
+                               cnstr_is_owner(c), c.get_justification(), relax_main_opaque(c));
+    }}
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
 }

src/library/util.h

@@ -159,6 +159,13 @@ expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_k
     of local constants */
 bool has_expr_metavar_relaxed(expr const & e);
 
+/** \brief Instantiate metavariables occurring in the expressions nested in \c c.
+
+    \remark The justification associated with each assignment are *not* propagaged.
+    We assume this is not a problem since we only used this procedure when connecting the
+    elaborator with the tactic framework. */
+constraint instantiate_metavars(constraint const & c, substitution & s);
+
 void initialize_library_util();
 void finalize_library_util();
 }

tests/lean/hott/trunc_1.hlean

@@ -0,0 +1,32 @@
+open is_trunc
+
+inductive trunc (n : trunc_index) (A : Type) : Type :=
+tr {} : A → trunc n A
+
+axiom is_trunc_tr (n : trunc_index) (A : Type) : is_trunc n (trunc n A)
+
+attribute is_trunc_tr [instance]
+
+namespace trunc
+  definition trunc_rec_on {n : trunc_index} {A : Type} {P : trunc n A → Type} (aa : trunc n A)
+    [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : P aa :=
+  trunc.rec_on aa H
+
+  definition trunc_functor1 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
+  begin
+    intro xx,
+    apply (trunc_rec_on xx),
+    intro x,
+    exact (tr (f x))
+  end
+
+  definition trunc_functor2 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
+  by intro xx; exact (trunc_rec_on xx (λx, (tr (f x))))
+
+  definition trunc_functor3 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
+  by exact (λxx, trunc_rec_on xx (λx, tr (f x)))
+
+  definition trunc_functor4 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
+  by intro xx; apply (trunc_rec_on xx); intro x; exact (tr (f x))
+
+end trunc