test-->> fails to detect alpha-equivalent cycles

[wilbowma]

Might be related to #102

This comes up in the Amb tutorial if you adapt the language to use binding forms, causing students to become very confused.

#lang racket

(require redex/reduction-semantics)

(define-language λL
  (e v
     x
     (e e)
     (λ (x) e)
     (fix e))
  (E hole (E e) (v E) (fix E))
  (v number)
  (x variable-not-otherwise-mentioned)

  #:binding-forms
  (λ (x) e #:refers-to x))

(define ->value
  (reduction-relation
   λL
   #:domain e
   (--> (in-hole E ((λ (x) e) v))
        (in-hole E (mf-apply substitute e x v))
        "EV-beta")
   (--> (in-hole E (fix (λ (x) e)))
        (in-hole E (mf-apply substitute e x (fix (λ (x) e))))
        "EV-fix")))

(module+ test
  (require rackunit)
  (check (curry alpha-equivalent? λL)
         (first
          (apply-reduction-relation ->value
    (first (apply-reduction-relation ->value (term ((fix (λ (x) x)) 1))))))
   (term ((fix (λ (x) x)) 1)))

  (let ([t (thread
            (lambda ()
              (check-exn
               exn:fail?
               (lambda ()
                 (test-->>
                  ->value #:cycles-ok
                  (term ((fix (λ (x) x)) 1)))))))])
    (check-true
     (sync/timeout 5 t))
    (kill-thread t)))