fix: have simpa ... using ... do exact-like checks

Closes leanprover#5634. Before assigning the `using` clause expression to the goal, this adds a check that the expression has no new metavariables. It also admits the goal when we report new metavariables since asserting the term as a new hypothesis causes it to be linked to pre-existing goals, leading to "don't know how to synthesize placeholder" errors for them. We also throw in an occurs check immediately after elaboration to avoid some counterintuitive behavior with simp.

src/Lean/Elab/Tactic/Simpa.lean

@@ -46,22 +46,35 @@ deriving instance Repr for UseImplicitLambdaResult
           return {}
       g.withContext do
       let stats ← if let some stx := usingArg then
-        setGoals [g]
-        g.withContext do
+        let mvarCounterSaved := (← getMCtx).mvarCounter
         let e ← Tactic.elabTerm stx none (mayPostpone := true)
-        let (h, g) ← if let .fvar h ← instantiateMVars e then
-          pure (h, g)
-        else
-          (← g.assert `h (← inferType e) e).intro1
+        unless ← occursCheck g e do
+          throwError "occurs check failed, expression{indentExpr e}\ncontains the goal {Expr.mvar g}"
+        let (h, g) ←
+          if let .fvar h := e then
+            pure (h, g)
+          else
+            (← g.assert `h (← inferType e) e).intro1
         let (result?, stats) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
           (simplifyTarget := false) (stats := stats) (discharge? := discharge?)
         match result? with
         | some (xs, g) =>
-          let h := match xs with | #[h] | #[] => h | _ => unreachable!
-          let name ← mkFreshBinderNameForTactic `h
-          let g ← g.rename h name
-          g.assign <|← g.withContext do
-            Tactic.elabTermEnsuringType (mkIdent name) (← g.getType)
+          setGoals [g]
+          g.withContext do
+            let h := Expr.fvar (xs[0]?.getD h)
+            let gType ← g.getType
+            let hType ← inferType h
+            unless (← withAssignableSyntheticOpaque <| isDefEq gType hType) do
+              Term.throwTypeMismatchError none gType hType h
+            let unassigned ← filterOldMVars (← getMVars e) mvarCounterSaved
+            unless unassigned.isEmpty do
+              -- Admit the goal to ensure that the original goal metavariable doesn't turn up with an error.
+              -- Recall that `logUnassignedAndAbort` says a metavariable could not be synthesized if
+              -- the instantiated metavariable contains one of the metavariables from the `unassigned` array.
+              admitGoal g
+              logUnassignedAndAbort unassigned
+              throwError m!"expression contains metavariables{indentExpr e}"
+            closeMainGoal `simpa (checkUnassigned := false) h
         | none =>
           if getLinterUnnecessarySimpa (← getOptions) then
             if (← getLCtx).getRoundtrippingUserName? h |>.isSome then

tests/lean/run/4920.lean

@@ -16,7 +16,7 @@ but is expected to have type
   A : outParam (Type _)
 ---
 error: type mismatch
-  h✝
+  ih
 has type
   i < as.length : Prop
 but is expected to have type

tests/lean/run/5634.lean

@@ -0,0 +1,54 @@
+/-!
+# Make sure `simpa` checks for metavariables in `using` clause
+
+https://github.com/leanprover/lean4/issues/5634
+-/
+
+/-!
+This used to have a "don't know how to synthesize placeholder" error on the `have` line too.
+This is because `have` is `refine_lift have ...; ?_`, so it indeed had a placeholder.
+-/
+/--
+error: don't know how to synthesize placeholder for argument 'a'
+context:
+htrue : True
+⊢ False
+-/
+#guard_msgs in
+example : False := by
+  have htrue : True := trivial
+  simpa using id _
+
+/-!
+Simplified version of the test.
+-/
+/--
+error: don't know how to synthesize placeholder for argument 'a'
+context:
+⊢ False
+-/
+#guard_msgs in
+example : False := by
+  refine ?_
+  simpa using id ?_
+
+/-!
+Verifying that unassigned metavariables are OK, so long as they come from before elaboring the `using` clause.
+-/
+example (p : Prop) (h : p) : p := by
+  have : ?a := ?b
+  simpa using ?b
+  exact h
+
+/-!
+Occurs check
+-/
+/--
+error: occurs check failed, expression
+  ?foo
+contains the goal ?foo
+-/
+#guard_msgs in
+example : False := by
+  refine ?foo
+  simpa using ?foo