substitute and alpha-equivalent? not working for typed grammar

[wilbowma]

Below are two grammars, identical except for type annotations on variables. In the untyped grammar, substitute and alpha-equivalent? behave as expected. In the typed grammar, they do not.

#lang racket/base
(require redex/reduction-semantics)

(define-language L
  (e ::= x (λ (x) e) (e e))
  (x ::= variable-not-otherwise-mentioned)

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

(module+ test
  (require rackunit)
  (default-language L)
  (check-true
   (alpha-equivalent? (term (λ (x) e))  (term (λ (x) e))))
  (check-true
   (alpha-equivalent? (term (λ (x) x))  (term (λ (y) y))))
  (check-false
   (alpha-equivalent? (term (λ (x) y))  (term (λ (y) y))))

  (check-true
   (alpha-equivalent?
    (term (substitute (λ (y) (x e2)) x (y z)))
    (term (λ (x) ((y z) e2))))))

(define-language tL
  (e ::= x (λ (x : A) e) (e e))
  (A B ::= b (→ A B))
  (x ::= variable-not-otherwise-mentioned)

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

(module+ test
  (default-language tL)
  (check-true
   (alpha-equivalent? (term (λ (x : A) e))  (term (λ (x : A) e))))
  ; fails
  (check-true
   (alpha-equivalent? (term (λ (x : A) x))  (term (λ (y : A) y))))
  (check-false
   (alpha-equivalent? (term (λ (x : A) y))  (term (λ (y : A) y))))

  ; fails
  (check-true
   (alpha-equivalent?
    (term (substitute (λ (y : A) (x e2)) x (y z)))
    (term (λ (x : A) ((y z) e2))))))

[wilbowma]

This was my fault for committing the deadly sin of variable/meta-variable punning.