This is such a cool idea.<p>One potential application is doing something like F#'s type providers for typed access to a SQL database.<p>You could use `trivial` to get fully typed SELECT statements integrated with Typed Racket.<p>In fact, Ben has already done some thinking along these lines: section 3.6 of <a href="http://www.ccs.neu.edu/home/types/cv/failures/icfp-2016-reject.pdf" rel="nofollow">http://www.ccs.neu.edu/home/types/cv/failures/icfp-2016-reje...</a> sketches out the idea, and there is some stubbed-out code in the `trivial` git repo waiting to be dusted off.