Type check modules.  Things seem to work.
Make the tests work.

Note that now interaction with Agda is getting more complicated -- `open
import Prelude` is interpreted by `tog`.  Moreover, I don't want to make
an effort in mimicking the record behaviour, since we're probably going
to change it anyway.

Note that the released `bnfc` is buggy, and the git `bnfc` is buggy, so
while <https://github.com/BNFC/bnfc/pull/116> gets merged you need my
version of `bnfc`: <https://github.com/BNFC/bnfc/pull/116>.