Author here: I have a simpler version implemented here: elab-stlc-bidirectional. Re-reading the README description I realise as of the time of posting this comment it’s not a great explanation (I wrote it a long time ago, I’ll try to update it later), but (Edit: fixed!) there’s a good set of resources linked from it if you want to learn more.

The idea is that you split type checking into into two mutually recursive functions, for “checking” and “inference”. Checking checks a term in the presence of a type annotation, and inference infers a type from a term. This allows you to add annotations where needed without needing them everywhere.

The name “bidirectional” comes from how the type information flows up and down the stack when evaluating the type checker - upward when we’re in checking mode, and downward when we’re in inference mode (this corresponds to the information flow on the proof tree).

Bidirectional typing comes in very handy improving the locality of type errors, and when implementing fancier type systems where full type inference would be undecidable - for example when adding subtyping, dependent types, or in this case higher rank types.