{-# LANGUAGE GADTs,RankNTypes #-}
data T a where T1 :: (forall b. b -> b) -> (forall a. Int -> T a)
{- Error:
Data constructor `T1' returns type `forall a. Int -> T a'
instead of an instance of its parent type `T a'
This looks to me like other cases where GHC requires an exact type match even though you used something equivalent. Similarly, for example, it rejects (contrived example)
foo :: Num a => a -> a -> a
foo 0 0 = -1
foo = (+)
because the explicit arity of the cases must match exactly, even though (+)'s type matches the required arity. I am under the impression that it's difficult to make those kinds of things work nicely in the typechecker.