feat: improve elabMatchAux

We now (try to) postpone `match ... with` elaboration when pattern
variables and patterns still contain metavariables before invoking `mkMatcher`.

This improvement makes sure we can elaborate an example submitted by
Daniel Selsam.

Remark: this update may create performance problems since we
backtrack `elabMatchTypeAndDiscrs` and `elabMatchAltView`.
We hope this is not a problem in practice since we use the "quick-check"
`waitExpectedTypeAndDiscrs`. Recall that we could compile Lean
without this commit. So, it suggests cases where we need to postpone
after `elabMatchAltView` are rare.

src/Lean/Elab/Match.lean

@@ -708,44 +708,64 @@ def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) :
 
 private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltView) (matchOptType : Syntax) (expectedType : Expr)
     : TermElabM Expr := do
-  let (discrs, matchType, altViews) ← elabMatchTypeAndDiscrs discrStxs matchOptType altViews expectedType
-  let matchAlts ← liftMacroM $ expandMacrosInPatterns altViews
-  trace[Elab.match]! "matchType: {matchType}"
-  let alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType
-  /-
-   We should not use `synthesizeSyntheticMVarsNoPostponing` here. Otherwise, we will not be
-   able to elaborate examples such as:
-   ```
-   def f (x : Nat) : Option Nat := none
+  let (discrs, matchType, altLHSS, rhss) ← commitIfDidNotPostpone do
+    let (discrs, matchType, altViews) ← elabMatchTypeAndDiscrs discrStxs matchOptType altViews expectedType
+    let matchAlts ← liftMacroM $ expandMacrosInPatterns altViews
+    trace[Elab.match]! "matchType: {matchType}"
+    let alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType
+    /-
+     We should not use `synthesizeSyntheticMVarsNoPostponing` here. Otherwise, we will not be
+     able to elaborate examples such as:
+     ```
+     def f (x : Nat) : Option Nat := none
 
-   def g (xs : List (Nat × Nat)) : IO Unit :=
-   xs.forM fun x =>
-     match f x.fst with
-     | _ => pure ()
-   ```
-   If `synthesizeSyntheticMVarsNoPostponing`, the example above fails at `x.fst` because
-   the type of `x` is only available after we proces the last argument of `List.forM`.
+     def g (xs : List (Nat × Nat)) : IO Unit :=
+     xs.forM fun x =>
+       match f x.fst with
+       | _ => pure ()
+     ```
+     If `synthesizeSyntheticMVarsNoPostponing`, the example above fails at `x.fst` because
+     the type of `x` is only available after we proces the last argument of `List.forM`.
 
-   We apply pending default types to make sure we can process examples such as
-   ```
-   let (a, b) := (0, 0)
-   ```
-  -/
-  synthesizeSyntheticMVarsUsingDefault
-  let rhss := alts.map Prod.snd
-  let matchType ← instantiateMVars matchType
-  let altLHSS ← alts.toList.mapM fun alt => do
-    let altLHS ← Match.instantiateAltLHSMVars alt.1
-    withRef altLHS.ref do
-      for d in altLHS.fvarDecls do
-        if d.hasExprMVar then
-          withExistingLocalDecls altLHS.fvarDecls do
-            throwMVarError m!"invalid match-expression, type of pattern variable '{d.toExpr}' contains metavariables{indentExpr d.type}"
-      for p in altLHS.patterns do
-        if p.hasExprMVar then
-          withExistingLocalDecls altLHS.fvarDecls do
-            throwMVarError m!"invalid match-expression, pattern contains metavariables{indentExpr (← p.toExpr)}"
-      pure altLHS
+     We apply pending default types to make sure we can process examples such as
+     ```
+     let (a, b) := (0, 0)
+     ```
+    -/
+    synthesizeSyntheticMVarsUsingDefault
+    let rhss := alts.map Prod.snd
+    let matchType ← instantiateMVars matchType
+    let altLHSS ← alts.toList.mapM fun alt => do
+      let altLHS ← Match.instantiateAltLHSMVars alt.1
+      /- Remark: we try to postpone before throwing an error.
+         The combinator `commitIfDidNotPostpone` ensures we backtrack any updates that have been performed.
+         The quick-check `waitExpectedTypeAndDiscrs` minimizes the number of scenarios where we have to postpone here.
+         Here is an example that passes the `waitExpectedTypeAndDiscrs` test, but postpones here.
+         ```
+          def bad (ps : Array (Nat × Nat)) : Array (Nat × Nat) :=
+            (ps.filter fun (p : Prod _ _) =>
+              match p with
+              | (x, y) => x == 0)
+            ++
+            ps
+         ```
+         When we try to elaborate `fun (p : Prod _ _) => ...` for the first time, we haven't propagated the type of `ps` yet
+         because `Array.filter` has type `{α : Type u_1} → (α → Bool) → (as : Array α) → optParam Nat 0 → optParam Nat (Array.size as) → Array α`
+         However, the partial type annotation `(p : Prod _ _)` makes sure we succeed at the quick-check `waitExpectedTypeAndDiscrs`.
+      -/
+      withRef altLHS.ref do
+        for d in altLHS.fvarDecls do
+            if d.hasExprMVar then
+            withExistingLocalDecls altLHS.fvarDecls do
+              tryPostpone
+              throwMVarError m!"invalid match-expression, type of pattern variable '{d.toExpr}' contains metavariables{indentExpr d.type}"
+        for p in altLHS.patterns do
+          if p.hasExprMVar then
+            withExistingLocalDecls altLHS.fvarDecls do
+              tryPostpone
+              throwMVarError m!"invalid match-expression, pattern contains metavariables{indentExpr (← p.toExpr)}"
+        pure altLHS
+    return (discrs, matchType, altLHSS, rhss)
   let numDiscrs := discrs.size
   let matcherName ← mkAuxName `match
   let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS

src/Lean/Elab/Term.lean

@@ -206,11 +206,20 @@ def getMessageLog : TermElabM MessageLog :=
 /--
   Apply the result/exception and state captured with `observing`.
   We use this method to implement overloaded notation and symbols. -/
-def applyResult (result : TermElabResult α) : TermElabM α :=
+@[inline] def applyResult (result : TermElabResult α) : TermElabM α :=
   match result with
   | EStateM.Result.ok a r     => do r.restore; pure a
   | EStateM.Result.error ex r => do r.restore; throw ex
 
+/--
+  Execute `x`, but keep state modifications only if `x` did not postpone.
+  This method is useful to implement elaboration functions that cannot decide whether
+  they need to postpone or not without updating the state. -/
+def commitIfDidNotPostpone (x : TermElabM α) : TermElabM α := do
+  -- We just reuse the implementation of `observing` and `applyResult`.
+  let r ← observing x
+  applyResult r
+
 @[inline] protected def liftMetaM {α} (x : MetaM α) : TermElabM α :=
   liftM x
 

tests/lean/forErrors.lean.expected.out

@@ -1,4 +1,2 @@
 forErrors.lean:3:29-3:30: error: failed to synthesize instance
   ToStream α ?m
-forErrors.lean:5:15-5:39: error: failed to synthesize instance
-  ToString α

tests/lean/run/Daniel1.lean

@@ -0,0 +1,17 @@
+def small (ps : Array (Nat × Nat)) : Array (Nat × Nat) :=
+  (ps.filter fun (p : Prod _ _) =>
+    match p with
+    | (x, y) => x == 0)
+  ++
+  ps
+
+#eval small #[(1, 2), (0, 3), (2, 4)]
+
+variables {α β : Type} [Inhabited α] [Inhabited β]
+
+def P (xys : Array (α × β)) (f : α → β) : Prop := True
+
+example (xys : Array (α × β))
+        (pred? : α → Bool)
+        (H : Subtype $ P (xys.filter fun (x, _) => pred? x))
+        : Unit := ()