In some cases, match stucks in an endless loop during compile time.

[NoahStoryM]

What version of Racket are you using?

v7.8

What program did you run?

#lang typed/racket

(define-type Lambda (U 'λ 'lambda))
(define-predicate λ? Lambda)

(define-type KeyWord (U Lambda 'quote))
(define-type Variable (Refine [var : Symbol] (! var KeyWord)))
(define-predicate variable? Variable)

(define-type S-Exp (U Variable
                      (List 'quote S-Exp)
                      (List Lambda (List Variable) S-Exp)
                      (Listof S-Exp)))
(define-predicate s-exp? S-Exp)


(match (ann '(lambda (y) y) S-Exp)
  [`(,(? λ?) (,(? variable? x)) ,(? s-exp? body))
   (displayln (cons x body))]

  [`(,(? variable? op) ,(? s-exp? a) ,(? s-exp? b))
   (displayln `(,op ,a ,b))]

  [`(,op ,a)
   (and (variable? op)
        (s-exp? a))])

What should have happened?

(y . y)

If you got an error message, please include it here.

Every branch of match stucks in an endless loop.
(I'm not sure why they caused an endless loop, so I just put code here)

Following code works:

(match (ann '(λ (y) y) S-Exp)
  [`(λ (,(? variable? x)) ,(? s-exp? body))
   (displayln (cons x body))]

  [`(,(? symbol? op) ,(? s-exp? a) ,(? s-exp? b))
   (displayln `(,op ,a ,b))])