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).