built in type lit type families that could be injective *should* be injective
make type lits useful sans solvers
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?