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
newtypeto represent the dictionaries for classes that have just a single method and no super-classes.
SingIis just such a class.
Singis already a
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.