@RyanGlScott I didn't know about this ticket, but I'd seen something on the mailing lists about this, and Lennart Augustsson mentioned at ICFP that they'd find something like this useful, so I figured I'd implement it. Do we really need quot and rem? I though these only differ on -ve numbers, and here we are working with natural numbers. I did wonder about adding DivMod but figured that it would inconvenient to project from type-level pairs... Not sure. I know in Cryptol we find it useful to also have round-up division and modulus, as these are exactly what you need when chunking a sequence of something into fixed-size blocks, to compute the number of blocks and the padding respectively. Perhaps we could add these in the future.
Indeed, for Nat we would have Quot = Div, Rem = Mod, and QuotRem = DivMod. I was suggesting that perhaps we could define type Quot = Div (and similarly for the other two) for the sake of parity with the value-level versions that are offered. Then again, I suppose this would be easy enough for users to define, so perhaps it's not so important to define those in base. I'll leave it up to your discretion.
I did wonder about adding DivMod but figured that it would inconvenient to project from type-level pairs...
To be clear, I don't suggest implementing Div and Mod in terms of DivMod. For raw speed, I think it would be best to implement Div and Mod in terms of their value-level counterpats div and mod, and make DivMod its own thing (in terms of divMod). Then we wouldn't have to define, say, Fst and Snd to project out of it at the type level.