feat: ensure #eval converts unassigned universe metavars into param…

…eters see #898
leanprover · Dec 20, 2021 · b278a20 · b278a20
1 parent 51dc329
commit b278a20
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.DocString
+import Lean.Util.CollectLevelParams
 import Lean.Elab.Command
 import Lean.Elab.Open
 
@@ -296,10 +297,13 @@ unsafe def elabEvalUnsafe : CommandElab
     let n := `_eval
     let ctx ← read
     let addAndCompile (value : Expr) : TermElabM Unit := do
+      let (value, _) ← Term.levelMVarToParam (← instantiateMVars value)
       let type ← inferType value
+      let us := collectLevelParams {} value |>.params
+      let value ← instantiateMVars value
       let decl := Declaration.defnDecl {
         name        := n
-        levelParams := []
+        levelParams := us.toList
         type        := type
         value       := value
         hints       := ReducibilityHints.opaque

diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
@@ -2,10 +2,10 @@ Sum.someRight c : Option Nat
 evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
   @Sum.someRight ?m Nat c
 context:
-⊢ Type ?u
+⊢ Type u_1
 evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
   @c ?m
 context:
-⊢ Type ?u
+⊢ Type u_1
 Sum.someRight c : Option Nat
 Sum.someRight c : Option Nat