fix(frontends/lean/elaborator): unsolved metavariables, fix #329

src/frontends/lean/elaborator.cpp

@@ -1292,7 +1292,7 @@ pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, exp
     lean_assert(p);
     substitution s  = p->first.first;
     constraints rcs = p->first.second;
-    r = s.instantiate(r);
+    r = s.instantiate_all(r);
     r = solve_unassigned_mvars(s, r);
     copy_info_to_manager(s);
     return mk_pair(r, rcs);

src/kernel/metavar.cpp

@@ -142,6 +142,7 @@ protected:
     cache_ref      m_cache;
     justification  m_jst;
     bool           m_use_jst;
+    // if m_inst_local_types, then instantiate metavariables nested in the types of local constants and metavariables.
     bool           m_inst_local_types;
 
     void save_jst(justification const & j) { m_jst = mk_composite1(m_jst, j); }
@@ -187,7 +188,10 @@ protected:
                 return p2.first;
             }
         } else {
-            return m;
+            if (m_inst_local_types)
+                return update_mlocal(m, visit(mlocal_type(m)));
+            else
+                return m;
         }
     }
 

src/kernel/metavar.h

@@ -70,7 +70,7 @@ public:
     level instantiate(level const & l) { return instantiate_metavars(l, false).first; }
 
     /** \brief Instantiate metavariables occurring in \c e, by default this method does not visit the
-        types of local constants.
+        types of local constants and metavariables.
         For substituting the metavariables occurring in local constants, use instantiate_metavars_all.
     */
     pair<expr, justification> instantiate_metavars(expr const & e) { return instantiate_metavars_core(e, false); }
@@ -78,7 +78,7 @@ public:
     pair<expr, justification> instantiate_metavars_all(expr const & e) { return instantiate_metavars_core(e, true); }
     /** \brief Similar to \c instantiate_metavars, but does not compute a justification for the substitutions. */
     expr instantiate(expr const & e) { return instantiate_metavars_wo_jst(e, false); }
-    /** \brief Similar to instantiate, but also substitute metavariables occurring in the types of local constansts */
+    /** \brief Similar to instantiate, but also substitute metavariables occurring in the types of local constansts and metavariables */
     expr instantiate_all(expr const & e) { return instantiate_metavars_wo_jst(e, true); }
 
     void forget_justifications() { m_expr_jsts  = jst_map(); m_level_jsts = jst_map(); }

tests/lean/run/329.lean

@@ -0,0 +1,20 @@
+import hott data.sigma
+open path sigma
+
+variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
+          {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
+
+definition path_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b') : dpair a b ≈ dpair a' b' :=
+path.rec_on p (λb b' q, path.rec_on q idp) b b' q
+
+definition path_sigma (p :  dpr1 u ≈ dpr1 v) (q : p ▹ dpr2 u ≈ dpr2 v) : u ≈ v :=
+destruct u
+         (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
+         p q
+
+definition path_path_sigma_lemma' {p1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : p1 ▹ b ≈ b'}
+    (s : idp ▹ p2 ≈ q2) : path_sigma p1 p2 ≈ path_sigma p1 q2 :=
+begin
+  apply (path.rec_on s),
+  apply idp,
+end