diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 3a9d32af64..c04e6bad90 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/tests/lean/run/4555.lean b/tests/lean/run/4555.lean
new file mode 100644
index 0000000000..31f90c309d
--- /dev/null
+++ b/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