fix(tactic/delta_instance): handle universe metavariables (leanprover…

…-community#2463)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/meta/expr.lean

@@ -158,6 +158,18 @@ meta def nonzero : level → bool
 | (imax _ l₂) := l₂.nonzero
 | _ := ff
 
+/--
+`l.fold_mvar f` folds a function `f : name → α → α`
+over each `n : name` appearing in a `level.mvar n` in `l`.
+-/
+meta def fold_mvar {α} : level → (name → α → α) → α → α
+| zero f := id
+| (succ a) f := fold_mvar a f
+| (param a) f := id
+| (mvar a) f := f a
+| (max a b) f := fold_mvar a f ∘ fold_mvar b f
+| (imax a b) f := fold_mvar a f ∘ fold_mvar b f
+
 end level
 
 /-! ### Declarations about `binder` -/
@@ -309,6 +321,15 @@ e.fold mk_name_set (λ e' _ es, if e'.is_constant then es.insert e'.const_name e
 meta def list_meta_vars (e : expr) : list expr :=
 e.fold [] (λ e' _ es, if e'.is_mvar then insert e' es else es)
 
+/-- Returns a list of all universe meta-variables in an expression (without duplicates). -/
+meta def list_univ_meta_vars (e : expr) : list name :=
+native.rb_set.to_list $ e.fold native.mk_rb_set $ λ e' i s,
+match e' with
+| (sort u) := u.fold_mvar (flip native.rb_set.insert) s
+| (const _ ls) := ls.foldl (λ s' l, l.fold_mvar (flip native.rb_set.insert) s') s
+| _ := s
+end
+
 /--
 Test `t` contains the specified subexpression `e`, or a metavariable.
 This represents the notion that `e` "may occur" in `t`,

src/tactic/core.lean

@@ -234,6 +234,18 @@ do subst ← d.univ_params.mmap $ λ u, prod.mk u <$> mk_meta_univ,
    let e : expr := expr.const d.to_name (prod.snd <$> subst),
    return (e, d.type.instantiate_univ_params subst)
 
+/--
+Replace every universe metavariable in an expression with a universe parameter.
+
+(This is useful when making new declarations.)
+-/
+meta def replace_univ_metas_with_univ_params (e : expr) : tactic expr :=
+do
+  e.list_univ_meta_vars.enum.mmap (λ n, do
+    let n' := (`u).append_suffix ("_" ++ to_string (n.1+1)),
+    unify (expr.sort (level.mvar n.2)) (expr.sort (level.param n'))),
+  instantiate_mvars e
+
 /-- `mk_local n` creates a dummy local variable with name `n`.
 The type of this local constant is a constant with name `n`, so it is very unlikely to be
 a meaningful expression. -/
@@ -1805,6 +1817,7 @@ do new_decl_type ← declaration.type <$> get_decl new_decl_name,
    (_, inst) ← solve_aux tgt
      (intros >> reset_instance_cache >> delta_target [new_decl_name]  >> apply_instance >> done),
    inst ← instantiate_mvars inst,
+   inst ← replace_univ_metas_with_univ_params inst,
    tgt ← instantiate_mvars tgt,
    nm ← get_unused_decl_name $ new_decl_name ++
      match cls with

test/delta_instance.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
 import data.set
+import algebra.category.Mon.basic
 
 @[derive has_coe_to_sort] def X : Type := set ℕ
 
@@ -22,3 +23,8 @@ instance : binclass ℤ ℤ := ⟨⟩
 @[derive decidable_eq] def S := ℕ
 
 @[derive decidable_eq] inductive P | a | b | c
+
+open category_theory
+
+-- Test that `delta_instance` works in the presence of universe metavariables.
+attribute [derive large_category] Mon