[throwawaymaths]

Maybe you don't have to encode everything in the type system?

Also: Maybe not everything goes in the compiler?