I can use SomeSing with great effect to be able to dynamically generate Singletons and then pattern-match on them to be able to do fun stuff
> let x = SomeSing SFalse :: SomeSing ('KProxy :: KProxy Bool)
-- pretend x is dynamically generated using IO or something
> case x of SomeSing SFalse -> blah blah
SomeSing STrue -> blah blah
However, I'm not really sure how to do this with SNat, which is the data family instance for Sing Nat. One issue I have is that I'm not able to ever get the SNat data constructor in scope even when importing all of the relevant modules (Data.Singletons, Data.Singletons.TypeLits, Data.Singletons.Prelude, etc.) and enabling the extensions (even though SNat the constructor shows up when I use :browse and :i Sing)
...another issue I have is that ... there aren't any separate constructors to match on like for SFalse and STrue...there's just one constructor! :O How am I supposed to use this in the same way?
I believe the problem is that there are two natural number singleton types both called SNat. The one you seem to have found goes with GHC typelits. Its constructor is not exported from the defining module, but it's an Integer underneath. You can access that integer, but the whole thing seems to be pretty much useless for proofs. The other SNat version deals with the classic Peano naturals. It'll work for proofs, but will be slow at runtime. I've not yet seen a Haskell natural good for both proofs and speed.