polymorphic instantiation of universally quantified types in type constructors gets accepted depending on the order of arguments
Assume we have the following definition:
{-# LANGUAGE ImpredicativeTypes, GADTSyntax #-}
data T2 a b where
K2 :: a -> T2 a a
-- accepted
h1 :: T2 (forall c. c -> c) b -> (Char, Bool)
h1 (K2 x) = (x 'z', x True)
-- rejected
h2 :: T2 b (forall c. c -> c) -> (Char, Bool)
h2 (K2 x) = (x 'z', x True)
h2
gets rejected, while h1
doesn't; when in fact, both of them should be rejected!