Richard are you satisfied that my example program is invalid under PolyKinds?
Yes. But I think as we've started to piece together, the real problem in this example is a missing superclass constraint on Typeable, not a fundamental shortcoming of PolyKinds. (I do acknowledge that extra polymorphism can introduce trouble, but given the fact that PolyKinds introduces parametric polymorphism -- unlike the ad hoc polymorphism of OverloadedStrings -- I think these cases should be rare.)
It would be interesting to see whether fixing Typeable in this way fixes other problems Chris has run into.
Richard