implementation

The only "magic" thing about GHC.TypeLits are the instances of SingI. The rest is implemented like this:

newtype Sing n = Sing (SingRep n)

type family SingRep a
type instance SingRep (n :: Nat) = Integer
type instance SingRep (n :: Symbol) = String

fromSing :: Sing n -> SingRep n 
fromSing (Sing n) = n

So, now we just need instances like these:

instance SingI 0       where sing = Sing 0
instance SingI 1       where sing = Sing 1
instance SingI "hello" where sing = Sing "hello"
...

Because we cannot generate this infinite family of instances, we have some code in GHC which can solve SingI predicates on the fly.

The "proof" (aka "dictionary") for SingI n is just the number (or string) n. This is OK because:

GHC uses a newtype to represent the dictionaries for classes that have just a single method and no super-classes. SingI is just such a class.
Sing is already a newtype for Integer or String, depending on the kind of its parameter.

Therefore, the dictionaries for class SingI are just integers or strings, depending on the kind of the parameter.