Term-reflection of TypeLits/Nats type-families
Now as there are SNat
, SSymbol
, SChar
in the base
it has ingredients to also define term-reflections, e.g.
(+) :: SNat n -> SNat m -> SNat (n + m) -- or plusSNat
E.g. constraints has plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
, which could be safely defined using plusSNat
.
It would be great to constraint the "trusted" source to the base
(i.e. library defining the magic type-families).
The #23478 issue is related. I cannot defined plusSNat
without doing unsafeCoerce
magic outside base
. But, if plusSNat
were defined, I'd not care about SNat
constructor being exported too much (it would be nice, anyway).