Hi, I am trying to define a type-and-effect system for the lambda calculus extended with raise and with-handlers. I am however stuck on the typing rule for with-handlers:

(define-typed-syntax (with-handlers ([p handler]) e) ≫ [⊢ e ≫ e- (⇒ : τ-e) (⇒ exn (~locs e-exn ...))] [⊢ p ≫ p- (⇒ : τ-p (⇒ exn (~locs p-exn ...)))] [(→ τ-e Bool) τ= τ-p #:for p] [⊢ handler ≫ handler- (⇒ : τ-handler (⇒ exn (~locs handler-exn ...)))] [τ-handler τ= (→ τ-e τ-e) #:for handler] ;; #:with uncaught-exn (remove (syntax->list #'(e-exn ...)) p) -------------------- [⊢ (with-handlers- ([p- handler-]) e-) (⇒ : τ-e) (⇒ exn (e-exn ... p-exn ... handler-exn ...))]) 1. To compute the effect of (with-handlers ...), I need to compute {exn ∈ exns-of-e \| ¬ (p exn)} , but I don’t know how to convert p into a Racket function. 2. To check the type of p, I used a turnstile syntax [... τ= ...]. A test code cause an error: with-handlers: type mismatch ; expected: (→ Int Bool) ; given: (→ Int Bool) ; expressions: (λ ((x : Int)) (< 0 x)) ; at: (with-handlers (((λ ((x : Int)) (< 0 x)) (λ ((x : Int)) (raise 12)))) (+ (raise 17) (raise -1))) ; in: (with-handlers (((λ ((x : Int)) (< 0 x)) (λ ((x : Int)) (raise 12)))) (+ (raise 17) (raise -1))) Could anyone give me some advice?