I like number option number two. I don't really expect any of the TypeInType stuff to work with the deriving machinery. I think that, at the moment, for a normal deriving clause, GHC never adds in constraints (I might be wrong on this). Whenever constraints, I feel like StandaloneDeriving is the right choice. I don't know if StandaloneDeriving works with DeriveFunctor or not, but if it does, then this is what I would expect:
REJECTED
data Proxy k (a :: k) = P
deriving Functor
ACCEPTED
data Proxy k (a :: k) = P
deriving instance (k ~ *) => Functor Proxy k
But if the second code snippet involving StandaloneDeriving can't be made to work, I would still prefer for the first snippet to be rejected as well. Just my two cents.
-Andrew Thaddeus Martin