check-redundancy and the O(n^n) bubblesort

The following test code demonstrates a common issue.

#lang racket

(require redex/reduction-semantics)

(check-redundancy #t)

(define-language L
  [ xs ::= (n ...) ]
  [ n ::= natural ]
  )

(define-metafunction L
  bubblesort : xs -> xs
  [(bubblesort (n_1 ... n_2 n_3 n_4 ...))
   (bubblesort (n_1 ... n_3 n_2 n_4 ...))
   (side-condition (< (term n_2) (term n_3)))
   ]
  [(bubblesort xs) xs]
  )

(define (shuffle xs)
  (sort xs < #:key (λ (x) (random)) #:cache-keys? #t))


(define xs (shuffle (stream->list (in-range 100))))

(define-syntax-rule (time f)
  (begin
    (define t0 (current-seconds))
    (println f)
    (println (- (current-seconds) t0))
    ))

(for ([ i (in-range 100) ])
  (time (term (bubblesort ,(take xs i)))))

The bubblesort metafunction has an ambiguous pattern match. So redex will evaluate all possible normalization paths and check that they return the same result, which is O(n^(n^2))

The check-redundancy parameter is supposed to catch ambiguous matches, but I've never gotten any output from it.

Additionally, many metafunctions - such as AST simplifiers or bubblesorts - are expected to reduce to the same result no matter what order the pattern matches are taken in. Is there a way to commit to the first successful match, which in this example would reduce the runtime to O(n^3)?

Start by running the supplied Racket example and tracing the check-redundancy parameter with the bubblesort metafunction. Determine why no redundancy diagnostic appears and investigate whether a first-match mode is supported. Done means the ambiguity behavior and requested commit semantics are clearly reproduced and covered by tests.