DataKinds and type class instances

Question

The following example is a boiled-down version of my real-life problem. It seems to be in some way similar to Retrieving information from DataKinds constrained existential types, but I could not quite get the answers I was seeking.

Suppose we have a finite, promoted DataKind K with types A and B, and a poly-kinded Proxy data-type to generate terms with types of kind *.

{-# LANGUAGE DataKinds, PolyKinds, GADTs, FlexibleInstances, FlexibleContexts #-}

data K = A | B

data Proxy :: k -> * where Proxy :: Proxy k

Now I want to write Show-instances for every type Proxy a where a is of kind K, which are exactly two:

instance Show (Proxy A) where show Proxy = "A"
instance Show (Proxy B) where show Proxy = "B"

But to use the Show-instance, I have to explicitly provide the context, even if the kind is restricted to K:

test :: Show (Proxy a) => Proxy (a :: K) -> String
test p = show p

My goal is to get rid of the type-class constraint. This may seem unimportant, but in my real application, this has major implications.

I could also define a single, but more general Show-instance like this:

instance Show (Proxy (a :: K)) where show p = "?"

This actually allows me to drop the constraint, but the new problem is to differentiate between the two types A and B.

So, is there a way to eat my cake and have it too? That is, not having to provide a type-class constraint in the type of test (kind annotations are fine, though), and still having two different show implementations (e.g. by differentiating the types somehow)?

Actually, it would also be okay to drop the entire type class, if I could simply associate the respective types (A, B) with their specific values (here: "A", "B") in a context where I just have the type information. I have no idea how to do this, though.

I would be very thankful for any provided insights.

Answer 1

No, this is not possible. In a context where you have "just the type information", at run-time, you really have no information. Type information is erased. So even for closed kinds, where it is in principle possible to show that given the type in question, you can always come up with a dictionary, you still need the class constraint. The class constraint ensures that at compile time, when GHC knows the type, it can select the appropriate instance to pass along. At run-time, the information which type it is is lost, and there's no chance to do the same. Writing a "one size fits all" instance does indeed work, because then the exact type does not matter for the choice anymore.

I don't know the full picture, but it may be possible to work around this by explicitly bundling up either the class dictionary or the string itself with the value you are passing around ...