I posted this on Discord, but I'm very proud of this, even if it is largely just a translation of the implementation provided by Coquand et al.'s Mini-TT.
Here's the repo: GitHub - hanleyc01/rkttt
It's largely undocumented, but the main algorithm is in tc.rkt - I'm working on some documentation that helps with understanding exactly how the program works, but either way implementing it has helped me a lot in understanding bidirectional typechecking 
.
If you do look at it, I apologize for if anything is ugly or unreadable, or if there are some dead ends that don't lead anywhere (/nanopass-experiment/, e.g.). Either way, this was the most fun I've had working on a project, and some of the most fun I've had playing with my computer ever.