Should SNat, SSymbol and SChar constructors be exported from some Unsafe module?
Let say I want to implement function:
plusSNat :: SNat n -> SNat m -> SNat (n + m)
I think I'm out-of-luck, and currently I would need to use unsafeCoerce
? Having constructors exported would enable writing unsafeCoerce
as demonstrated in #23454 (closed), so the "power" and "responsibility" are similar, but just using constructors directly would at least make implementations of functions like plusSNat
clearer.
Ping @RyanGlScott