Using these types we can define functions that are overloaded based on their kind (rather than type).
An example of such a function is fromSing, which given an element of a singleton family returns the run-time
value representing the singleton. This function uses kind overloading because it uses the same representation
for all singletons of a given kind. For example, here are two concrete instances of its type:
fromSing :: Sing (a :: Nat) -> IntegerfromSing :: Sing (a :: Symbol) -> String
Here is how we can define fromSing in its full generality:
class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where type DemoteRep kparam :: * fromSing :: Sing (a :: k) -> DemoteRep kparam
Here are the different components of this declaration:
The class has a single parameter kparam, which is of kind OfKind k.
The super-class constraint makes it explicit that the value of the parameter will always be KindParam
(One we eliminate Any, GHC could probably work this out on its own, but for now we make this explicit.)
The associated type synonym DemoteRep chooses the representation for singletons of the given kind.
Finally, the method fromSing maps singletons to their representation.
This might look a bit complex, but defining instances is pretty simple. Here are some examples:
instance SingE (KindParam :: OfKind Nat) where type DemoteRep (KindParam :: OfKind Nat) = Integer fromSing (SNat n) = ninstance SingE (KindParam :: OfKind Symbol) where type DemoteRep (KindParam :: OfKind Symbol) = String fromSing (SSym s) = s
It is convenient to define another type synonym, which lets us name
the representation type for a given singleton: