The algorithm is split into two mutual components the "inference" and the "checking" (upward and downward) which run together. This turns out to be a really fle

The algorithm is split into two mutual components the "inference" and the "checking" (upward and downward) which run together. This turns out to be a really flexible setting for playing with language and type features as it's often possible to figure out how to extend a bidirectional typer/inferrer with new features.