4.1.5 Function calls
Under "static analysis" second para it says "The first rule
bootstraps...".  It is not clear whether "first rule" is a
backward reference to the first sentence of the preceding
paragraph ("To typecheck a Core function call we first check...")
or a forward refernce to the inference presented immediately
following the subject sentence.  From the use of colons it becomes
clear that you must mean the inference that follows.  Still,
the reader may waste a lot of effort trying to correlate the
two "first"s, thinking perhaps that the inference is a formalization
of the first paragraph's first sentence.  To avoid this, it 
would be better to use the more precise term "inference" instead
of "rule" (this suggestion could be carried out throughout the 
entire specification) and you might also avoid the word "first".
Thus the sentence might begin "The following inference...".