Internal error in modeless `define-judgment-form` when only some judgments have ellipses

[laelath]

The following program errors with .../racket/pkgs/redex-lib/redex/private/modeless-jf.rkt:94:71: define-judgment-form: found any under 2 ellipses in one place and 1 ellipsis in another. I found that adding more premises with ellipses works fine, but this error appears as soon as there are both premise judgments with and without ellipses.

#lang racket

(require redex/reduction-semantics)

(define-language L
  (n ::= natural)
  (e ::= n x +)
  (t ::= num)
  (tf ::= ((t ...) -> (t ...)))
  (C ::= ((x tf) ...))
  (x ::= variable-not-otherwise-mentioned)
  (mod ::= ([x (func tf (e ...))] ...)))

(define-judgment-form L
  #:contract (⊢ C (e ...) tf)

  [-----------------------
   (⊢ C (n) (() -> (num)))]

  [------------------------------
   (⊢ C (+) ((num num) -> (num)))]

  [(where (_ ... (x tf) _ ...) C)
   ------------------------------
   (⊢ C (x) tf)])

(define-judgment-form L
  #:contract (same-context C (C ...))
  #:mode (same-context I I)

  [-------------------
   (same-context _ ())]

  [(same-context C_1 (C_2 ...))
   --------------------------------
   (same-context C_1 (C_1 C_2 ...))])

(define-judgment-form L
  #:contract (⊢-mod mod C)

  [(where ((x tf) ...) C)
   (⊢ C_f (e ...) tf) ...
   (same-context C (C_f ...))
   -------------------------------------
   (⊢-mod ([x (func tf (e ...))] ...) C)])

I found a very hacky way to get around this.

(define-judgment-form L
  #:contract (⊢-mod-badfix mod C)

  [(where ((x tf) ...) C)
   (⊢ C_f (e ...) tf) ...
   (where (C_1 ...) (C))
   (where ((C_2 ...) ...) ((C_f ...)))
   (same-context C_1 (C_2 ...)) ...
   -------------------------------------
   (⊢-mod-badfix ([x (func tf (e ...))] ...) C)])

[rfindler]

Here's a minimized example. The problem has to do with the ellipses that appears between the premises. That ellipsis is handled specially compared to the others.

#lang racket
(require redex/reduction-semantics)

(define-language L)

(define-judgment-form L
  #:contract (⊢ any)
  #:mode (⊢ I)
  [-------
   (⊢ any)])

(define-judgment-form L
  #:contract (⊢-mod any)

  [(⊢ (2 ...)) ...
   (⊢ 1)
   ----------------
   (⊢-mod 1)])