Right now, we have some manual definitions for things like combining positive integers where the operation could result in an exit from the domain. We should save ourselves the code and instead rely on iron's instances of the necessary typeclasses, since our refined types are now built with iron.