strictly positive checker

strictly-positive.rkt

#lang racket
(require syntax/parse/define
         (for-syntax syntax/stx))

(begin-for-syntax
  (define-syntax-class type
    #:datum-literals (->)
    (pattern (~literal Type)
      #:attr occurs (λ (D) #f))
    (pattern x:id
      #:attr occurs (λ (D)
                      (eq? (syntax->datum D)
                           (syntax->datum #'x))))
    (pattern (t1:type -> t2:type)
      #:attr occurs (λ (D)
                      (or ((attribute t1.occurs) D)
                          ((attribute t2.occurs) D)))))

  (define-syntax-class constructor
    #:datum-literals (:)
    (pattern (name:id : ty:type)
      #:attr check-strictly-positive
      (λ (D)
        (syntax-parse #'ty
          #:datum-literals (->)
          ; a type in Pi form
          [(L:type -> R:type)
           (syntax-parse #'L
             [(L:type -> R:type)
              (not ((attribute L.occurs) D))]
             [else #t])]
          ; or we don't care
          [_ #t])))))

(define-syntax-parser data
  [(_ name:id : ty:type
      c*:constructor ...)
   (for-each (λ (check c)
               (unless (check #'name)
                 (raise-syntax-error 'data-type
                                     (format "~a is not strictly positive" (syntax->datum #'name))
                                     c)))
             (attribute c*.check-strictly-positive)
             (syntax->list #'(c* ...)))
   #'(void)])

(data Nat : Type
      [z : Nat]
      [s : (Nat -> Nat)])

(data Bad : Type
      [bad : ((Bad -> Bad) -> Bad)])