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 anewtype
forInteger
orString
, 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.