Made the module pass the totality checker
Implemented most of `contract`; one metavar remains