feat: improve error message

when match-expression LHSs still contain metavariables after elaboration

src/Lean/Elab/Match.lean

@@ -748,12 +748,23 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi
    ```
   -/
   synthesizeUsingDefault
-  -- TODO report error if matchType or altLHSS.toList have metavars
   let rhss := alts.map Prod.snd
-  let altLHSS := alts.map Prod.fst
+  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
+            throwError! "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
+            throwError! "invalid match-expression, pattern contains metavariables{indentExpr (← p.toExpr)}"
+      pure altLHS
   let numDiscrs := discrs.size
   let matcherName ← mkAuxName `match
-  let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS.toList
+  let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS
   let motive ← forallBoundedTelescope matchType numDiscrs fun xs matchType => mkLambdaFVars xs matchType
   reportMatcherResultErrors matcherResult
   let r := mkApp matcherResult.matcher motive

src/Lean/LocalContext.lean

@@ -85,6 +85,10 @@ def updateBinderInfo : LocalDecl → BinderInfo → LocalDecl
 def toExpr (decl : LocalDecl) : Expr :=
   mkFVar decl.fvarId
 
+def hasExprMVar : LocalDecl → Bool
+  | cdecl (type := t) ..              => t.hasExprMVar
+  | ldecl (type := t) (value := v) .. => t.hasExprMVar || v.hasExprMVar
+
 end LocalDecl
 
 open Std (PersistentHashMap PersistentArray PArray)

src/Lean/Meta/Match/Match.lean

@@ -66,13 +66,35 @@ def replaceFVarId (fvarId : FVarId) (v : Expr) (p : Pattern) : Pattern :=
   let s : FVarSubst := {}
   p.applyFVarSubst (s.insert fvarId v)
 
+partial def hasExprMVar : Pattern → Bool
+  | inaccessible e => e.hasExprMVar
+  | ctor _ _ ps fs => ps.any (·.hasExprMVar) || fs.any hasExprMVar
+  | val e          => e.hasExprMVar
+  | as _ p         => hasExprMVar p
+  | arrayLit t xs  => t.hasExprMVar || xs.any hasExprMVar
+  | _              => false
+
 end Pattern
 
+partial def instantiatePatternMVars : Pattern → MetaM Pattern
+  | Pattern.inaccessible e      => return Pattern.inaccessible (← instantiateMVars e)
+  | Pattern.val e               => return Pattern.val (← instantiateMVars e)
+  | Pattern.ctor n us ps fields => return Pattern.ctor n us (← ps.mapM instantiateMVars) (← fields.mapM instantiatePatternMVars)
+  | Pattern.as x p              => return Pattern.as x (← instantiatePatternMVars p)
+  | Pattern.arrayLit t xs       => return Pattern.arrayLit (← instantiateMVars t) (← xs.mapM instantiatePatternMVars)
+  | p                   => return p
+
 structure AltLHS :=
   (ref        : Syntax)
   (fvarDecls  : List LocalDecl) -- Free variables used in the patterns.
   (patterns   : List Pattern)   -- We use `List Pattern` since we have nary match-expressions.
 
+def instantiateAltLHSMVars (altLHS : AltLHS) : MetaM AltLHS :=
+  return { altLHS with
+    fvarDecls := (← altLHS.fvarDecls.mapM instantiateLocalDeclMVars),
+    patterns  := (← altLHS.patterns.mapM instantiatePatternMVars)
+  }
+
 structure Alt :=
   (ref       : Syntax)
   (idx       : Nat) -- for generating error messages

tests/lean/match1.lean

@@ -1,4 +1,4 @@
-
+--
 
 #print "---- h1"
 
@@ -120,3 +120,11 @@ match n, parity n with
 | _, Parity.odd  j => true  :: natToBin j
 
 #eval natToBin2 6
+
+#check fun (a, b) => a -- Error type of pattern variable contains metavariables
+
+#check fun (a, b) => (a:Nat) + b
+
+#check fun (a, b) => a && b
+
+#check fun ((a : Nat), (b : Nat)) => a + b

tests/lean/match1.lean.expected.out

@@ -19,3 +19,6 @@ match1.lean:113:0: error: dependent match elimination failed, inaccessible patte
   .(j + j)
 constructor expected
 [false, true, true]
+match1.lean:124:0: error: invalid match-expression, type of pattern variable 'a' contains metavariables
+  ?m
+fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m