This puts the constraint on the wrong thing.
I did argue for a pragma-like syntax for the annotations when they were first proposed, as the need for library authors to hide these behind CPP pragmas bothers me a great deal, but I think for better or worse that syntax decision is largely behind us.
A type-class driven approach does have some promise, but that said, it can't look like what you've written.
What you've written:
data Nominal k => Map k a
is saying something about the argument k, not about if you can turn Map k into Map k', which is actually about Map, k is just along for the ride.
Really what we're talking about is that the next argument is representational as applied. Also, the right 'open world' version would be to talk about it as classes would be:
class Representational t where
rep :: Coercion a b -> Coercion (t a) (t b)
class Representational t => Phantom t where
phantom :: Coercion (t a) (t b)
With "Nominal" simply being the absence of either of those instances.
data Map k a
would need
instance Representational (Map k)
since the 'a' can be coerced as it has a representational role.
instance Representational (->)
instance Representational ((->) a)
But there are actually still open issues I don't know how to solve, even with this approach.
-Edward