Knowing that:
a is of kind K- the only types of kind
K are A and B
Show (Proxy A) holdsShow (Proxy B) holds
is sufficient to prove that Show (Proxy a) holds. But a type class isn't just a proposition that we need to prove true to use with our type, it also provides implementations. To actually use show (x :: Proxy a) we need to not just prove that an implementation for Show (Proxy a) exists, we need to actually know which one it is.
Haskell type variables (without constraints) are parametric: there's no way to be fully polymorphic in a, and also be able to inspect a to provide different behaviour for A and B. The "different behaviour" you want is about as "close to parametric" as you can possibly be without actually being parametric, since it's just the selection of a different instance for each type when you know there is one for each type. But it's still something that breaks the contract of what test :: forall (a :: K). Proxy a -> String means.
Type class constraints allow your code to be non-parametric in the constrained type variables, in as much as you can use the type class' mapping from types to implementations to switch how your code behaves based on the type it's invoked at. So test :: forall (a :: K). Show (Proxy a) => Proxy a -> String works. (In terms of the actual implementation, the same ultimate caller who gets to choose the type a also provides the Show (Proxy a) instance for the code generated from your function to use).
You can use your instance Show (Proxy (a :: K)) idea; now your function that is parametric in a type a :: K can still use show (x :: Proxy a) because there is one instance that works for all a :: K. But the instance itself runs into the same problem; the implementation of show in the instance is parametric in a, and so can't inspect it in anyway in order to return a different string based on the type.
You can use something like dfeuer's answer, where Kish exploits the non-parametricity of constrained type variables to basically allow you to inspect the type at runtime; the instance dictionary passed along to satisfy the Kish a constraint basically is a run time record of which type was chosen for the variable a (in a roundabout way). Pushing this idea further gets you all the way to Typeable. But you still need some sort of constraint to make your code non-parametric in a.
You can also use a type that is explicitly a runtime representation of the choice of A or B (as opposed to Proxy, which is an empty value at runtime and only provides a compile-time representation of the choice), something like:
{-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving #-}
data K = A | B
data KProxy (a :: K)
where KA :: KProxy A
KB :: KProxy B
deriving instance Show (KProxy a)
test :: KProxy a -> String
test = show
(Note here I can not only implement Show (Kproxy a), I can actually derive it, although it does require standalone deriving)
This is using a GADT KProxy to allow test to be non-parametric in a, essentially doing the same job as the Kish constraint from dfeuer's answer but avoiding the need to add an extra constraint to your type signatures. In an earlier version of this post I stated that test was able to do this while remaining "just" parametric in a, which was incorrect.
Of course now to pass a proxy you have to actually write KA or KB. That's no bother where you were having to write Proxy :: Proxy A to actually choose the type (which is often the case with proxies, given that you usually only use them to fix a type that otherwise would be ambiguous). But where it would have been unambiguous anyway the compiler will catch you if you're inconsistent with the rest of the call, but you can't write just one symbol like Proxy and have the compiler infer the correct meaning. You can address that with a type class:
class KProxyable (a :: K)
where kproxy :: KProxy a
instance KProxyable A
where kproxy = KA
instance KProxyable B
where kproxy = KB
Then you can use KA instead of Proxy :: Proxy A, and kproxy instead of letting the compiler infer the type of a bare Proxy. Stupid example time:
foo :: KProxy a -> KProxy a -> String
foo kx ky = show kx ++ " " ++ show ky
GHCI:
λ foo KA kproxy
"KA KA"
Note I'm not actually needing to have a KProxyable constraint anywhere; I use kproxy at a point where the type is known. This still has to "come in from the top", though (exactly as the instance dictionary satisfying your Show (Proxy a) constraint would); there's no way to have a function parametric in a type a :: K come up with the relevant KProxy a on its own.
Because it's the correspondence between the constructors and the type that makes this work, I don't believe you can make a generic proxy in this style the way you can with the empty-at-runtime Proxy. TemplateHaskell could certainly generate such proxy types for you though; I think the concept of singletons is the general idea here, and so the https://hackage.haskell.org/package/singletons probably provides what you need, but I'm not very familiar with how to actually use that package.
