It does seem unnecessary. The Data instance for Proxy is manually written in Data.Data:
proxyConstr :: Constr
proxyConstr = mkConstr proxyDataType "Proxy" [] Prefix
proxyDataType :: DataType
proxyDataType = mkDataType "Data.Proxy.Proxy" [proxyConstr]
instance (Data t) => Data (Proxy t) where
gfoldl _ z Proxy = z Proxy
toConstr Proxy = proxyConstr
gunfold _ z c = case constrIndex c of
1 -> z Proxy
_ -> error "Data.Data.gunfold(Proxy)"
dataTypeOf _ = proxyDataType
dataCast1 f = gcast1 f
If dataCast1 weren't defined to be gcast1, then that instance would only require a Typeable t constraint, which would make it polykinded. To be honest, I'm not sure why gcast1 requires a Data t constraint (I don't use Data that often, so hopefully someone more knowledgeable than me can answer this).