Q: How to implement equi-recursive types in PLT Redex? I believe that I understand both equi-recursive and iso-recursive types quite well. Hence, I've been trying to implement a type checker for ISWIM with equi-recursive types in PLT Redex. However, for the life of me I can't figure out how to make type equivalence work. Everything else works great.
This is my language:
(define-language iswim
  [X  ::= variable-not-otherwise-mentioned]
  [b  ::= number true false unit]
  [O  ::= + - * =]
  [M  ::= b X (λ (X : T) M) (M M) (if M M M) (O M M)
      (pair M M) (fst M) (snd M) (inL M T) (inR M T)
      (match M (λ (X : T) M) (λ (X : T) M))]
  [V  ::= b (λ (X : T) M) (pair V V) (inL V T) (inR V T)]
  [T  ::= X Unit Bool Num (T -> T) (T + T) (T × T) (μ (X) T)]
  [Γ  ::= () (X T Γ)]
  #:binding-forms
  (λ (X : T) M #:refers-to X)
  (μ (X) T #:refers-to X))

The type checker is a judgment form (I think the "App" case is wrong):
(define-judgment-form iswim
  #:mode (types I I O)
  #:contract (types Γ M T)

  [-------------------- "Number"
   (types Γ number Num)]

  [-------------------- "True"
   (types Γ true Bool)]

  [-------------------- "False"
   (types Γ false Bool)]

  [-------------------- "Unit"
   (types Γ unit Unit)]

  [(where T (lookup Γ X))
   -------------------- "Var"
   (types Γ X T)]

  [(types (X T_1 Γ) M T_2)
   -------------------- "Abs"
   (types Γ (λ (X : T_1) M) (T_1 -> T_2))]

  [(types Γ M_1 T_1)
   (types Γ M_2 T_2)
   (equiv-types T_1 (T_2 -> T_3))
   -------------------- "App"
   (types Γ (M_1 M_2) T_3)]

  [(types Γ M_1 Bool)
   (types Γ M_2 T)
   (types Γ M_3 T)
   -------------------- "If"
   (types Γ (if M_1 M_2 M_3) T)]

  [(types Γ M_1 Num)
   (types Γ M_2 Num)
   (where T (return-type O))
   -------------------- "Op"
   (types Γ (O M_1 M_2) T)]

  [(types Γ M_1 T_1)
   (types Γ M_2 T_2)
   -------------------- "Pair"
   (types Γ (pair M_1 M_2) (T_1 × T_2))]

  [(types Γ M (T_1 × T_2))
   -------------------- "First"
   (types Γ (fst M) T_1)]

  [(types Γ M (T_1 × T_2))
   -------------------- "Second"
   (types Γ (snd M) T_2)]

  [(types Γ M T_1)
   -------------------- "Left"
   (types Γ (inL M T_2) (T_1 + T_2))]

  [(types Γ M T_2)
   -------------------- "Right"
   (types Γ (inR M T_1) (T_1 + T_2))]

  [(types Γ M_3 (T_1 + T_2))
   (types (X_1 T_1 Γ) M_1 T_3)
   (types (X_2 T_2 Γ) M_2 T_3)
   -------------------- "Match"
   (types Γ (match M_3
              (λ (X_1 : T_1) M_1)
              (λ (X_2 : T_2) M_2))
              T_3)])

Type equivalence is another judgment form (I put all of the blame on this code):
(define-judgment-form iswim
  #:mode (equiv-types I I)
  #:contract (equiv-types T T)

  [-------------------- "Refl"
   (equiv-types T T)]

  [(equiv-types T_1 T_3)
   (equiv-types T_2 T_4)
   -------------------- "Fun"
   (equiv-types (T_1 -> T_2) (T_3 -> T_4))]

  [(equiv-types T_1 T_3)
   (equiv-types T_2 T_4)
   -------------------- "Sum"
   (equiv-types (T_1 + T_2) (T_3 + T_4))]

  [(equiv-types T_1 T_3)
   (equiv-types T_2 T_4)
   -------------------- "Prod"
   (equiv-types (T_1 × T_2) (T_3 × T_4))]

  [(where X_3 ,(variable-not-in (term (T_1 T_2)) (term X_2)))
   (equiv-types (substitute T_1 X_1 X_3) (substitute T_2 X_2 X_3))
   -------------------- "Mu"
   (equiv-types (μ (X_1) T_1) (μ (X_2) T_2))]

  [(equiv-types (substitute T_1 X (μ (X) T_1)) T_2)
   -------------------- "Mu Left"
   (equiv-types (μ (X) T_1) T_2)]

  [(equiv-types T_1 (substitute T_2 X (μ (X) T_2)))
   -------------------- "Mu Right"
   (equiv-types T_1 (μ (X) T_2))])

Here are my meta-functions:
(define-metafunction iswim
  lookup  : Γ X -> T or #f
  [(lookup () X)        #f]
  [(lookup (X T Γ) X)   T]
  [(lookup (X T Γ) X_1) (lookup Γ X_1)])

(define-metafunction iswim
  return-type : O -> T
  [(return-type +) Num]
  [(return-type -) Num]
  [(return-type *) Num]
  [(return-type =) Bool])

Any help will be appreciated.

A: I've never used PLT Redex and don't have it at hand, but let me answer since you write "[a]ny help will be appreciated".:-)  [Edited to add: I installed PLT Redex and implemented equi-recursive types. See below.]
As a general challenge with equi-recursive types, your algorithm would not work for a pair of types like
T1  =  (μ (X) (Bool -> X))
and
T2  =  (μ (X) (Bool -> (Bool -> X)))
for the following reason.  Suppose we compare T1 and T2 according to your algorithm as follows:
    T1  =?=  T2

By definition:
    (μ (X) (Bool -> X))  =?=  (μ (X) (Bool -> (Bool -> X)))

By looking into the bodies of the μ's as in your algorithm:
    (Bool -> X3)  =?=  (Bool -> (Bool -> X3))

By comparing the return types:
    X3  =?=  (Bool -> X3)

It thus fails to equate T1 and T2!
A correct algorithm should "memoioze" already visited type pairs, as follows:
    T1  =?=  T2

By definition:
    (μ (X) (Bool -> X))  =?=  (μ (X) (Bool -> (Bool -> X)))

By expanding the μ's remembering we have already visited T1 and T2:
    (Bool -> T1)  =?=  (Bool -> (Bool -> T2))  ***assuming T1 = T2***

By comparing the return types:
    T1  =?=  (Bool -> T2)  ***assuming T1 = T2***

By definition of T1:
    (μ (X) (Bool -> X))  =?=  (Bool -> T2)  ***assuming T1 = T2***

By expanding the μ on the l.h.s.:
    (Bool -> T1)  =?=  (Bool -> T2)  ***assuming T1 = T2***

By comparing the return types:
    T1  =?=  T2  ***assuming T1 = T2***

Yeah!
For theoretical details, see e.g. "Recursive subtyping revealed" by Gapeyev et al. (it considers subtyping but type equality is similar).
P.S.  My implementation in PLT Redex follows.  Save it in a file, open in DrRacket, and run.
    #lang racket
    (require redex)

    (define-language rectyp
      [X variable-not-otherwise-mentioned]
      [T ::= Bool Num (T -> T) (μ (X) T) X]
      [A ::= ・ (A T T)]
      #:binding-forms
      (μ (X) T #:refers-to X))

    (define-relation rectyp
      memo ⊆ A × T × T
      [(memo (A T_1 T_2) T_1 T_2)]
      [(memo (A T_1 T_2) T_3 T_4)
       (memo A T_3 T_4)])

    (define-relation rectyp
      equi-memo ⊆ A × T × T
      [(equi-memo A T_1 T_2)
       (memo A T_1 T_2)]
      [(equi-memo A T_1 T_2)
       (equi (A T_1 T_2) T_1 T_2)
       (side-condition (not (term (memo A T_1 T_2))))])

    ;; an alternative way to define equi-memo
    ;(define-metafunction rectyp
    ;  equi-memo : A T T -> boolean
    ;  [(equi-memo A T_1 T_2)
    ;   ,(or (term (memo A T_1 T_2))
    ;        (term (equi (A T_1 T_2) T_1 T_2)))])

    (define-relation rectyp
      equi ⊆ A × T × T
      [(equi A T T)]
      [(equi A (T_1 -> T_2) (T_3 -> T_4))
       (equi-memo A T_1 T_3)
       (equi-memo A T_2 T_4)]
      [(equi A (μ (X) T_1) T_2)
       (equi-memo A (substitute T_1 X (μ (X) T_1)) T_2)]
      [(equi A T_1 (μ (X) T_2))
       (equi-memo A T_1 (substitute T_2 X (μ (X) T_2)))])

    (term (equi-memo ・ (μ (X) (Num -> X)) (μ (X) (Num -> (Num -> X))))) ; #t

