fix: Make split work with metavariables in the target

The fix consists of replacing an internal use of `apply` for
instantiating match splitters by a new, simpler variant `applyN`. This
new `applyN` is not prone to #8436, which is the ultimate cause for
`split` failing on targets containing metavariables.

Author: Sebastian Graf

src/Lean/Meta/Tactic/Apply.lean

@@ -155,8 +155,8 @@ private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MV
   | ApplyNewGoals.all => return mvars.toList.map Lean.Expr.mvarId!
 
 /-- Custom `isDefEq` for the `apply` tactic -/
-private def isDefEqApply (cfg : ApplyConfig) (a b : Expr) : MetaM Bool := do
-  if cfg.approx then
+private def isDefEqApply (approx : Bool) (a b : Expr) : MetaM Bool := do
+  if approx then
     approxDefEq <| isDefEqGuarded a b
   else
     isDefEqGuarded a b
@@ -201,7 +201,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
       if i < rangeNumArgs.stop then
         let s ← saveState
         let (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType i
-        if (← isDefEqApply cfg eType targetType) then
+        if (← isDefEqApply cfg.approx eType targetType) then
           return (newMVars, binderInfos)
         else
           s.restore
@@ -231,6 +231,21 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
 def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   mvar.apply (← mkConstWithFreshMVarLevels c) cfg (term? := m!"'{.ofConstName c}'")
 
+/-- Close the given goal using `e`, instantiated with `n` metavariables. -/
+def _root_.Lean.MVarId.applyN (mvarId : MVarId) (e : Expr) (n : Nat) (useApproxDefEq := true) : MetaM (List MVarId) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `apply
+    let targetType ← mvarId.getType
+    let eType      ← inferType e
+    let (mvarIds, _, eType) ← forallMetaBoundedTelescope eType n
+    unless mvarIds.size == n do
+      throwError "Applied type takes fewer than {n} arguments:\n{indentExpr eType}"
+    unless (← isDefEqApply useApproxDefEq eType targetType) do
+      throwError "Type mismatch: target is\n{indentExpr targetType}\nbut applied expression has \
+        type\n{indentExpr eType}\nafter applying {n} arguments."
+    mvarId.assign (e.beta mvarIds)
+    return (mvarIds.map (·.mvarId!)).toList
+
 end Meta
 
 open Meta

src/Lean/Meta/Tactic/Split.lean

@@ -248,9 +248,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
     let splitter := mkAppN (mkApp splitter motive) discrsNew
     check splitter
     trace[split.debug] "after check splitter"
-    let mvarIds ← mvarId.apply splitter
-    unless mvarIds.length == matchEqns.size do
-      throwError "internal error in `split` tactic: unexpected number of goals created after applying splitter auxiliary theorem `{matchEqns.splitterName}` for `{matcherDeclName}`"
+    let mvarIds ← mvarId.applyN splitter matchEqns.size
     let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do
       let numParams := matchEqns.splitterAltNumParams[i]!
       let (_, mvarId) ← mvarId.introN numParams

tests/lean/split_mvars_target.lean

@@ -0,0 +1,15 @@
+/-!
+Tests that `split` works when there are metavariables in the target.
+-/
+theorem split_subgoals {x : Option Nat × Nat} :
+  match x.fst with
+  | some _ => True
+  | none => True
+  := by
+  have h {P : Prop} {x'} : (x' = 4 ∧ P) → P := by simp
+  apply h
+  split
+  rotate_right
+  · exact 4
+  · trivial
+  · trivial