fix: unused match-syntax alternatives are silently ignored

closes #1371

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* `match`-syntax notation now checks for unused alternatives. See issue [#1371](https://github.com/leanprover/lean4/issues/1371).
+
 * Auto-completion for structure instance fields. Example:
   ```lean
   example : Nat × Nat := {

src/Lean/Elab/ElabRules.lean

@@ -47,22 +47,22 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax
       `($[$doc?:docComment]? @[$attrKind:attrKind termElab $(← mkIdentFromRef k):ident]
         aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
         fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with
-          $alts:matchAlt* | _ => throwUnsupportedSyntax)
+          $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
     else
       throwErrorAt expId "syntax category '{catName}' does not support expected type specification"
   else if catName == `term then
     `($[$doc?:docComment]? @[$attrKind:attrKind termElab $(← mkIdentFromRef k):ident]
       aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
       fun stx _ => match stx with
-        $alts:matchAlt* | _ => throwUnsupportedSyntax)
+        $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
   else if catName == `command then
     `($[$doc?:docComment]? @[$attrKind:attrKind commandElab $(← mkIdentFromRef k):ident]
       aux_def elabRules $(mkIdent k) : Lean.Elab.Command.CommandElab :=
-      fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
+      fun $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
   else if catName == `tactic then
     `($[$doc?:docComment]? @[$attrKind:attrKind tactic $(← mkIdentFromRef k):ident]
       aux_def elabRules $(mkIdent k) : Lean.Elab.Tactic.Tactic :=
-      fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
+      fun $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
   else
     -- We considered making the command extensible and support new user-defined categories. We think it is unnecessary.
     -- If users want this feature, they add their own `elab_rules` macro that uses this one as a fallback.

src/Lean/Elab/MacroRules.lean

@@ -37,7 +37,7 @@ def elabMacroRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax
     | _ => throwUnsupportedSyntax
   `($[$doc?:docComment]? @[$attrKind macro $(Lean.mkIdent k)]
     aux_def macroRules $(mkIdentFrom tk k) : Macro :=
-     fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
+     fun $alts:matchAlt* | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax)
 
 @[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
   adaptExpander fun stx => match stx with

src/Lean/Elab/Quotation.lean

@@ -385,9 +385,11 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
           let contents := if contents.size == 1
             then contents[0]!
             else mkNullNode contents
+          -- We use `no_error_if_unused%` in auxiliary `match`-syntax to avoid spurious error messages,
+          -- the outer `match` is checking for unused alternatives
           `(match ($(discrs).sequenceMap fun
-                | `($contents) => some $tuple
-                | _            => none) with
+                | `($contents) => no_error_if_unused% some $tuple
+                | _            => no_error_if_unused% none) with
               | some $resId => $yes
               | none => $no)
     }
@@ -533,7 +535,7 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter
           -- group undecided alternatives in a new default case `| discr2, ... => match discr, discr2, ... with ...`
           let vars ← discrs.mapM fun _ => withFreshMacroScope `(discr)
           let pats := List.replicate newDiscrs.length (Unhygienic.run `(_)) ++ vars
-          let alts ← undecidedAlts.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => $(alt.2))
+          let alts ← undecidedAlts.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => no_error_if_unused% $(alt.2))
           let rhs  ← `(match discr, $[$(vars.toArray):term],* with $alts:matchAlt*)
           yesAlts := yesAlts.push (pats, rhs)
         withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts.toList)
@@ -543,15 +545,77 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter
     `(let discr := $discr; $stx)
   | _, _ => unreachable!
 
+abbrev IdxSet := Std.HashSet Nat
+
+/--
+Given `rhss` the right-hand-sides of a `match`-syntax notation,
+We tag them with with fresh identifiers `alt_idx`. We use them to detect whether an alternative
+has been used or not.
+The result is a triple `(altIdxMap, ignoreIfUnused, rhssNew)` where
+- `altIdxMap` is a mapping from the `alt_idx` identifiers to right-hand-side indices.
+  That is, the map contains the entry `alt_idx ↦ i` if `alt_idx` was used to mark `rhss[i]`.
+- `i ∈ ignoreIfUnused` if `rhss[i]` is marked with `no_error_if_unused%`
+- `rhssNew` is the updated array of right-hand-sides.
+-/
+private def markRhss (rhss : Array Term) : TermElabM (NameMap Nat × IdxSet × Array Term) := do
+  let mut altIdxMap : NameMap Nat := {}
+  let mut ignoreIfUnused : IdxSet := {}
+  let mut rhssNew := #[]
+  for rhs in rhss do
+    match rhs with
+    | `(no_error_if_unused% $_ ) => ignoreIfUnused := ignoreIfUnused.insert rhssNew.size
+    | _ => pure ()
+    let (idx, rhs) ← withFreshMacroScope do
+      let idx ← `(alt_idx)
+      let rhs ← `(alt_idx $rhs)
+      return (idx, rhs)
+    altIdxMap := altIdxMap.insert idx.getId rhssNew.size
+    rhssNew := rhssNew.push rhs
+  return (altIdxMap, ignoreIfUnused, rhssNew)
+
+/--
+Given the mapping `idxMap` built using `markRhss`, and `stx` the resulting syntax after expanding `match`-syntax,
+return the pair `(stxNew, usedSet)`, where `stxNew` is `stx` after removing the `alt_idx` markers in `idxMap`,
+and `i ∈ usedSet` if `stx` contains an `alt_idx` s.t. `alt_idx ↦ i` is in `idxMap`.
+That is, `usedSet` contains the index of the used match-syntax right-hand-sides.
+-/
+private partial def findUsedAlts (stx : Syntax) (altIdxMap : NameMap Nat) : TermElabM (Syntax × IdxSet) := do
+  go stx |>.run {}
+where
+  go (stx : Syntax) : StateRefT IdxSet TermElabM Syntax := do
+    match stx with
+    | `($id:ident $rhs:term) =>
+      if let some idx := altIdxMap.find? id.getId then
+        modify fun s => s.insert idx
+        return rhs
+    | _ => pure ()
+    match stx with
+    | .node info kind cs => return .node info kind (← cs.mapM go)
+    | _ => return stx
+
+/--
+Check whether `stx` has unused alternatives, and remove the auxiliary `alt_idx` markers from it (see `markRhss`).
+The parameter `alts` provides position information for alternatives.
+`altIdxMap` and `ignoreIfUnused` are the map and set built using `markRhss`.
+-/
+private def checkUnusedAlts (stx : Syntax) (alts : Array Syntax) (altIdxMap : NameMap Nat) (ignoreIfUnused : IdxSet) : TermElabM Syntax := do
+  let (stx, used) ← findUsedAlts stx altIdxMap
+  for i in [:alts.size] do
+    unless used.contains i || ignoreIfUnused.contains i do
+      logErrorAt alts[i]! s!"redundant alternative #{i+1}"
+  return stx
+
 def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
   match stx with
-  | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
+  | `(match $[$discrs:term],* with $[|%$alt $[$patss],* => $rhss]*) => do
     if !patss.any (·.any (fun
       | `($_@$pat) => pat.raw.isQuot
       | pat        => pat.raw.isQuot)) then
       -- no quotations => fall back to regular `match`
       throwUnsupportedSyntax
+    let (altIdxMap, ignoreIfUnused, rhss) ← markRhss rhss
     let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList
+    let stx ← checkUnusedAlts stx alt altIdxMap ignoreIfUnused
     trace[Elab.match_syntax.result] "{stx}"
     return stx
   | _ => throwUnsupportedSyntax
@@ -576,6 +640,11 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
 @[builtinTermElab «match»] def elabMatchSyntax : TermElab :=
   adaptExpander match_syntax.expand
 
+@[builtinTermElab noErrorIfUnused] def elabNoErrorIfUnused : TermElab := fun stx expectedType? =>
+  match stx with
+  | `(no_error_if_unused% $term) => elabTerm term expectedType?
+  | _ => throwUnsupportedSyntax
+
 builtin_initialize
   registerTraceClass `Elab.match_syntax
   registerTraceClass `Elab.match_syntax.result

tests/lean/1371.lean

@@ -0,0 +1,6 @@
+def f (stx : Lean.Syntax) :=
+  match stx with
+  | `($f $a)  => 1
+  | `($_)     => 2
+  | `($f $b)  => 3
+  | _         => "hello"

tests/lean/1371.lean.expected.out

@@ -0,0 +1,2 @@
+1371.lean:5:2-5:3: error: redundant alternative #3
+1371.lean:6:2-6:3: error: redundant alternative #4

tests/lean/StxQuot.lean

@@ -28,13 +28,13 @@ end Lean.Syntax
 #eval run $ do let a ← `(Nat.one); `($(a).b)
 #eval run $ do let a ← `(1 + 2); match a with | `($a + $b) => `($b + $a) | _ => pure miss
 #eval run $ do let a ← `(1 + 2); match a with | stx@`($a + $b) => `($stx + $a) | _ => pure miss
-#eval run $ do let a ← `(def foo := 1); match a with | `($f:command) => pure f | _ => pure miss
+#eval run $ do let a ← `(def foo := 1); match a with | `($f:command) => pure f
 #eval run $ do let a ← `(def foo := 1 def bar := 2); match a with | `($f:command $g:command) => `($g:command $f:command) | _ => pure ⟨Syntax.missing⟩
 
-#eval run $ do let a ← `(aa); match a with | `($_:ident) => pure 0 | `($_) => pure 1 | _ => pure 2
+#eval run $ do let a ← `(aa); match a with | `($_:ident) => pure 0 | `($_) => pure 1
 #eval match mkIdent `aa with | `(aa) => 0 | _ => 1
 #eval match mkIdent `aa with | `(ab) => 0 | _ => 1
-#eval run $ do let a ← `(1 + 2); match a with | `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
+#eval run $ do let a ← `(1 + 2); match a with | `($id:ident) => pure 0 | `($e) => pure 1
 #eval run $ do let params ← #[`(a), `((b : Nat))].mapM id; `(fun $params:term* => 1)
 #eval run $ do let a ← `(fun (a : Nat) b => c); match a with | `(fun $aa* => $e) => pure aa | _ => pure #[]
 #eval run $ do let a ← `(∀ a, c); match a with | `(∀ $id:ident, $e) => pure id | _ => pure ⟨a⟩

tests/lean/run/termParserAttr.lean

@@ -73,7 +73,7 @@ syntax (name := tst3) "FOO " foo : term
 macro_rules
 | `(FOO ⟨| $t |⟩) => `($t+1)
 | `(FOO $t:term) => `($t)
-| `(FOO $t:term >>> $r) => `($t * $r)
+
 
 #check FOO ⟨| id 1 |⟩
 #check FOO 1