Check for metavariables

src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean

@@ -140,7 +140,11 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
       let inst ← mkAppOptM ``CCPO.toPartialOrder #[type, ccpoInsts'[i]!]
       let goal ← mkAppOptM ``monotone #[packedType, packedPartialOrderInst, type, inst, F]
       if let some term := hints[i]!.term? then
-        Term.elabTermEnsuringType term goal
+        let hmono ← Term.withSynthesize <| Term.elabTermEnsuringType term goal
+        let hmono ← instantiateMVars hmono
+        if hmono.hasMVar then
+          throwErrorAt term "monotonicity proof must not contain meta variables{indentExpr hmono}"
+        pure hmono
       else
         let hmono ← mkFreshExprSyntheticOpaqueMVar goal
         mapError (f := (m!"Could not prove '{preDef.declName}' to be monotone in its recursive calls:{indentD ·}")) do

tests/lean/partial_fixpoint_parseerrors.lean

@@ -0,0 +1,17 @@
+
+-- Check that indent is required
+
+def nullary1 (x : Nat) : Option Unit := nullary1 (x + 1)
+partial_fixpoint monotonicity
+fun _ _ a x => a (x + 1)
+
+def nullary2 (x : Nat) : Option Unit := nullary2 (x + 1)
+partial_fixpoint
+monotonicity fun _ _ a x => a (x + 1)
+
+-- This is allowed:
+
+def nullary3 (x : Nat) : Option Unit := nullary3 (x + 1)
+partial_fixpoint
+    monotonicity
+  fun _ _ a x => a (x + 1)

tests/lean/partial_fixpoint_parseerrors.lean.expected.out

@@ -0,0 +1,2 @@
+partial_fixpoint_parseerrors.lean:6:0: error: expected indented monotonicity proof
+partial_fixpoint_parseerrors.lean:10:0-10:12: error: unexpected identifier; expected command

tests/lean/run/partial_fixpoint_explicit.lean

@@ -0,0 +1,62 @@
+/-!
+Tests for `partial_fixpoint` with explicit proofs
+-/
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+def nullary (x : Nat) : Option Unit := nullary (x + 1)
+partial_fixpoint monotonicity sorry
+
+-- Check for metavariables
+
+/--
+error: monotonicity proof must not contain meta variables
+  ?m.201
+-/
+#guard_msgs in
+def nullarya (x : Nat) : Option Unit := nullarya (x + 1)
+partial_fixpoint monotonicity _
+
+def nullaryb (x : Nat) : Option Unit := nullaryb (x + 1)
+partial_fixpoint monotonicity fun _ _ a _ => a _
+
+/-- info: nullaryb.eq_1 (x : Nat) : nullaryb x = nullaryb (x + 1) -/
+#guard_msgs in #check nullaryb.eq_1
+
+-- Type error
+
+/--
+error: type mismatch
+  ()
+has type
+  Unit : Type
+but is expected to have type
+  Lean.Order.monotone fun f x => f (x + 1) : Prop
+-/
+#guard_msgs in
+def nullary2 (x : Nat) : Option Unit := nullary2 (x + 1)
+partial_fixpoint monotonicity ()
+
+
+-- Good indent (bad indents are tested in partial_fixpoint_parseerrors
+
+def nullary4 (x : Nat) : Option Unit := nullary4 (x + 1)
+partial_fixpoint monotonicity
+  fun _ _ a x => a (x + 1)
+
+
+-- Tactics
+
+/-- info: Try this: exact fun x y a x => a (x + 1) -/
+#guard_msgs in
+def nullary6 (x : Nat) : Option Unit := nullary6 (x + 1)
+partial_fixpoint monotonicity by
+  exact?
+
+#guard_msgs in
+def nullary7 (x : Nat) : Option Unit := nullary7 (x + 1)
+partial_fixpoint monotonicity by
+  apply Lean.Order.monotone_of_monotone_apply
+  intro y
+  apply Lean.Order.monotone_apply
+  apply Lean.Order.monotone_id