would reduce to: `TypeError` or be irreducible i.e. be stuck?
I'm quite neutral about adding `Div` and `Mod` (after all, I added
-1 for `DivMod` (we need `Fst` and `Snd`in `base` too).
Yet, how about the rest of families in `Data.Constraint.Nat`  ?
1. Note: If we add them, let's only add them to GHC.TypeNats.
2. Note: current type families form decidable system, which
`ghc-typelits-natnormalize`  can solve. Adding division complicates
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 , 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
> Note: If we add them, let's only add them to GHC.TypeNats.
> 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.