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!

@simonpj @rae