`redex-check` doesn't warn about ellipsis in judgment-forms more than one level deep

[florence]

#lang racket
(require redex/reduction-semantics)

(define-language simple-plus
  (M (e e))
  (e natural))

(define-judgment-form simple-plus
  #:mode (okay1 I I)
  [
   --------
   (okay1 M (e ...))])

(define-judgment-form simple-plus
  #:mode (okay I)
  [(okay1 M ())
   --------
   (okay M)])

(redex-check simple-plus
 #:satisfying (okay e)
 (term e))

simply fails to generate terms. Note that if the okay in the redex-check is replaced with okay1 or if e is changes to have an ellipsis (ie changing e to (e ::= natural (+ e ...))) one gets the error (#:satisfying keyword does not support ellipses, contexts, side-conditions, or unquote)

[rfindler]

I think what's happening here is that define-judgment-form is smart enough to tell that this judgment form never produces an 'e' without getting tripped up by the ellipses. When I make modifications to it that cause the #:satisfying query to actually be non-empty, it always gets the error.

For example, if you try the judgment form below, it finds counterexamples.

#lang racket
(require redex/reduction-semantics)

(define-language simple-plus
  (M (any))
  (e natural))

(define-judgment-form simple-plus
  #:mode (okay1 I I)
  [
   --------------------------
   (okay1 any_1 (any_2 ...))])

(define-judgment-form simple-plus
  #:mode (okay I)

  [(okay1 M ())
   --------
   (okay M)]

  [--------
   (okay 1)])

(redex-check simple-plus
 #:satisfying (okay e)
 (= 2 (term e)))