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/75dae57bbe06b21b3adbb82158c476... [2] http://hackage.haskell.org/package/ghc-typelits-extra