feat: ensure no unassigned metavariables in the declaration header wh…

…en type is explicitly provided
leanprover · Jan 12, 2021 · 3600827 · 3600827
1 parent 3852ee1
commit 3600827
Show file tree

Hide file tree

Showing 7 changed files with 20 additions and 8 deletions.
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
@@ -102,9 +102,14 @@ private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHe
         elabBinders (catchAutoBoundImplicit := true) view.binders.getArgs fun xs => do
           let refForElabFunType := view.value
           elabFunType refForElabFunType xs view fun xs type => do
-            let type ← mkForallFVars (← read).autoBoundImplicits.toArray type
+            let mut type ← mkForallFVars (← read).autoBoundImplicits.toArray type
             let xs ← addAutoBoundImplicits xs
             let levelNames ← getLevelNames
+            if view.type?.isSome then
+              Term.synthesizeSyntheticMVarsNoPostponing
+              type ← instantiateMVars type
+              let pendingMVarIds ← getMVars type
+              discard <| logUnassignedUsingErrorInfos pendingMVarIds
             let newHeader := {
               ref           := view.ref,
               modifiers     := view.modifiers,

diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean
@@ -21,7 +21,7 @@ def check : Tree → UInt32
 
 def minN := 4
 
-def out (s) (n : Nat) (t : UInt32) : IO Unit :=
+def out (s : String) (n : Nat) (t : UInt32) : IO Unit :=
 IO.println (s ++ " of depth " ++ toString n ++ "\t check: " ++ toString t)
 
 -- allocate and check lots of trees

diff --git a/tests/lean/holeErrors.lean b/tests/lean/holeErrors.lean
@@ -1,4 +1,4 @@
-
+--
 
 def f1 := id
 

diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out
@@ -3,10 +3,6 @@ holeErrors.lean:3:10: error: don't know how to synthesize implicit argument
 context:
 ⊢ Sort u_1
 holeErrors.lean:3:7: error: failed to infer definition type
-holeErrors.lean:5:14: error: don't know how to synthesize implicit argument
-  @id ?m
-context:
-⊢ Sort u_1
 holeErrors.lean:5:9: error: failed to infer definition type
 holeErrors.lean:8:9: error: don't know how to synthesize implicit argument
   @id ?m

diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
@@ -419,5 +419,5 @@ def f3 x y :=
 theorem f3eq x y : f3 x y = x + y + 1 :=
   rfl
 
-def f4 x y : String :=
+def f4 (x y : Nat) : String :=
   if x > y + 1 then "hello" else "world"
diff --git a/tests/lean/theoremType.lean b/tests/lean/theoremType.lean
@@ -0,0 +1,5 @@
+theorem ex1 : 1 + 1 = _ := -- Error
+  show 1 + 1 = 2 by rfl
+
+def ex2 : 1 + 1 = _ := -- Error
+  show 1 + 1 = 2 by rfl
diff --git a/tests/lean/theoremType.lean.expected.out b/tests/lean/theoremType.lean.expected.out
@@ -0,0 +1,6 @@
+theoremType.lean:1:22: error: don't know how to synthesize placeholder
+context:
+⊢ Nat
+theoremType.lean:4:18: error: don't know how to synthesize placeholder
+context:
+⊢ Nat