There's a nasty wrinkle in our plan to use function identifiers as cost labels
for stack space.  The definition of programs we have allows function names to
shadow one another, with the earlier definition treated as totally irrelevant,
but still present in the block⇀fundef mapping of the global environment.  This
is benign in the sense that there's no way to construct a pointer with that
block, but breaks my attempt to provide a total mapping from blocks which we
happen to know map to functions to identifiers, because we don't have the
invariant that the block must have come from an unshadowed function.

These shadowed definitions are not permitted in standard C, and are rejected
during the transformation from the parser's output anyway.

Some possible solutions are:

 1 quietly drop shadowed functions from the block⇀fundef map when constructing
   the global environment; not terribly nice as they'll be carried through the
   whole compiler, but has low impact on everything
 2 use blocks for the stack cost labels; relies on setting up the environment
   in the same way each time - would have to be careful with the initialisation
   code, and reveals the internals a little bit much (that said, the program
   transformation results essentially do this)
 3 establish the invariant that shadowed functions' blocks never appear in
   program executions; probably a lot of work for little gain
 4 enforce distinct names, either in the program record (and hence on
   ‘importing’ Clight) or when creating the global environment; the latter may
   be a nuisance for the back-end because they use it as a total function
   (whereas the front-end also does initialisation which can already fail).