fix: .. in patterns should not make use of optparams or autoparams (#5933)

In patterns, ellipsis should always fill in each remaining argument as
an implicit argument, even if it is an optparam or autoparam. This
prevents examples such as the one in #4555 from failing:
```lean
match e with
| .internal .. => sorry
| .error .. => sorry
```
The `internal` constructor has an optparam (`| internal (id :
InternalExceptionId) (extra : KVMap := {})`).

We may consider having ellipsis suppress optparams and autoparams in
general. We avoid doing so for now since it's possible to opt-out of
them individually (for example with `.internal (extra := _) ..`) but
it's not possible to opt-in, and it is plausible that `..` with
optparams is useful in contexts such as the `refine` tactic. With
patterns however, it is hard to imagine a use case that offsets the
inconvenience of optparams being eagerly supplied.

Closes #4555

src/Lean/Elab/App.lean

@@ -595,6 +595,22 @@ mutual
       elabAndAddNewArg argName arg
       main
     | _ =>
+      if (← read).ellipsis && (← readThe Term.Context).inPattern then
+        /-
+        In patterns, ellipsis should always be an implicit argument, even if it is an optparam or autoparam.
+        This prevents examples such as the one in #4555 from failing:
+        ```lean
+        match e with
+        | .internal .. => sorry
+        | .error .. => sorry
+        ```
+        The `internal` has an optparam (`| internal (id : InternalExceptionId) (extra : KVMap := {})`).
+
+        We may consider having ellipsis suppress optparams and autoparams in general.
+        We avoid doing so for now since it's possible to opt-out of them (for example with `.internal (extra := _) ..`)
+        but it's not possible to opt-in.
+        -/
+        return ← addImplicitArg argName
       let argType ← getArgExpectedType
       match (← read).explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
       | false, some defVal, _  => addNewArg argName defVal; main

tests/lean/run/4555.lean

@@ -0,0 +1,16 @@
+import Lean.Exception
+/-!
+# In pattern, `..` shouldn't make use of opt-params
+
+https://github.com/leanprover/lean4/issues/4555
+-/
+
+open Lean
+
+/-!
+The `.internal` constructor has an opt-param, which caused this to be a non-exhaustive match.
+-/
+example (e : Exception) : Nat :=
+  match e with
+  | .internal .. => 0
+  | .error .. => 1