[racket] type assertions in plai-typed?

I’ve bitten the bullet and announced to my PL class that we’ll be using #lang plai-typed. Right now, I’m trying to figure out if there’s an easy way to do type debugging; in particular, I anticipate wanting to make assertions about the type of expressions that are buried inside of other expressions. Is there a form that allows me to do this? I had imagined that I could do it with ‘let’, but ‘let’ doesn’t take any type annotations.

Currently, the best I’ve got is an in-line application to an identity function with a type attached.  So, for instance, if I have this function

(define (id x)
  x)

… and I want to ensure that the expression ‘x’ has type number, I can write:


(define (id x)
  ((lambda ((z : number)) z) x))

… but that’s pretty painful. Is there an easier way? (Yes, I could add a type annotation to the declaration of ‘x’ and to the return type of the function, but I’m imagining a larger function where the expression in question is neither an argument to nor the result of the function.)

Many thanks,

John