Proposal: add integer division to GHC.TypeLits

[Ryan Scott]

To be clear, I don't think Alexey is proposing that we implement
inductive definitions of Div/Mod/DivMod to base (which, as you note,
would require implementing type-level Fst and Snd as well). One of the
motivations for this proposal is that we _did_ implement and inductive
DivMod in the singletons library [1], and it is horribly slow. What I
believe Alexey wants is a built-in type family that leverages machine
instructions to perform the div/mod calculations behind the hood, much
like we currently do for other type-level arithmetic operators, such
as (+), (-), and (*).

> Yet, how about the rest of families in `Data.Constraint.Nat`

Obviously, adding more built-in type families is perhaps not an ideal
solution, and there are certainly many more things we _could_ add. But
I think integer division is a common-enough use case that it makes
sense to support it in base. We need not bog down this proposal with
whataboutism.

> Note: If we add them, let's only add them to GHC.TypeNats.

Agreed.

> Note: current type families form decidable system, which
> `ghc-typelits-natnormalize` can solve. Adding division complicates
> that story.

Sure, but then again, there are many type families that you could
throw into this system that this particular GHC plugin couldn't reason
about. I don't see how Div/Mod are unique in that regard.

> What would be the semantics, especially what
>
>     Div n 0
>
> would reduce to: `TypeError` or be irreducible i.e. be stuck?

I would propose that it would be stuck. There is precedent for this
already: (2 - 3) is a stuck type, for instance. This is also the
approach that the ghc-typelits-extra plugin takes.

Ryan S.
-----
[1] https://github.com/goldfirere/singletons/blob/75dae57bbe06b21b3adbb82158c4767ebd695d14/src/Data/Singletons/Prelude/Show.hs#L201-L214
[2] http://hackage.haskell.org/package/ghc-typelits-extra