built in type lit type families that could be injective *should* be injective
Motivation
make type lits useful sans solvers
Proposal
https://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-TypeLits.html
AppendSymbol
+
*
-
and ^
all of these have clear "unique answer" or "should be error" semantics when any 2 of the pair of inputs and the output are specified
adding that extra knowledge to the type checker/inference machinery would also make it possible to write a "S :: Nat -> Nat" type family in user space that works as an injective type family too i think? (and thats a long running pain point that kills using them)
might also be good to think about other type level literals that should be in base. Eg type level integers?