Document the code/explain what is happening

[0x0f0f0f]

Im trying to read this together with the paper to reimplement this type system in go. Although the interpreter is simple, there are some things (like acronyms) that are not instantaneous to understand.
If you added some explanations of the internals in comments/github page it would be easier to reimplement and associate concepts/types/functions with the paper. Also, if you specified which rules are being applied in typecheck.ml it would also be a lot easier to associate pattern matching cases with the judgments in the paper.

For example, how are recursive functions achieved?