I see that the code in TypeCheck.Internal and Normalize.Internal contains gas computations. It seems unlikely that we're going to be doing typechecking on the chain, so should we remove the gas-related stuff eventually? That would simplify things a bit, which is probably good.