I recommend using quote-module-path and compiling your program with raco exe and raco dist.

Hello, everyone. Racket seems to hang forever in running the following code, #lang typed/racket/base (provide (all-defined-out)) (define-type (Formula a) (U True False (Atom a) (Not a) (And a) (Or a) (Imp a) (Iff a) (Forall a) (Exists a))) (struct False () #:transparent) (struct True () #:transparent) (struct (a) Atom ([f : a]) #:transparent) (struct (a) Not ([f : (Formula a)]) #:transparent) (struct (a) And ([l : (Formula a)] [r : (Formula a)]) #:transparent) (struct (a) Or ([l : (Formula a)] [r : (Formula a)]) #:transparent) (struct (a) Imp ([pre : (Formula a)] [post : (Formula a)]) #:transparent) (struct (a) Iff ([l : (Formula a)] [r : (Formula a)]) #:transparent) (struct (a) Forall ([v : String] [f : (Formula a)]) #:transparent) (struct (a) Exists ([v : String] [f : (Formula a)]) #:transparent) When I cut down the number of types in the union type, Racket finishes type checking.

Can you post an issue to <https://github.com/racket/typed-racket|the TR’s repo>?

Yes.