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 atype instance SingRep (n :: Nat) = Integertype instance SingRep (n :: Symbol) = StringfromSing :: Sing n -> SingRep n fromSing (Sing n) = n

So, now we just need instances like these:

instance SingI 0 where sing = Sing 0instance SingI 1 where sing = Sing 1instance 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.