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