Ah, I hadn't considered what effect nondeterminism might have on this. Here's a quick experiment: With normal uniques: $ /opt/ghc/8.0.1/bin/ghci -XTypeInType -fprint-explicit-kinds -fprint-explicit-foralls GHCi, version 8.0.0.20160411: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci λ> data T (a :: j -> k -> l) (b :: (x, y, z)) = MkT λ> :info T type role T nominal nominal nominal nominal nominal nominal phantom phantom data T x y z l k j (a :: j -> k -> l) (b :: (x, y, z)) = MkT -- Defined at <interactive>:1:1 λ> :type MkT MkT :: forall {x} {y} {z} {l} {k} {j} {a :: j -> k -> l} {b :: (x, y, z)}. T x y z l k j a b With reversed uniques: $ /opt/ghc/8.0.1/bin/ghci -XTypeInType -fprint-explicit-kinds -fprint-explicit-foralls -dunique-increment=-1 -dinitial-unique=16777000 GHCi, version 8.0.0.20160411: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci λ> data T (a :: j -> k -> l) (b :: (x, y, z)) = MkT λ> :info T type role T nominal nominal nominal nominal nominal nominal phantom phantom data T x y z l k j (a :: j -> k -> l) (b :: (x, y, z)) = MkT -- Defined at <interactive>:1:1 λ> :type MkT MkT :: forall {j} {k} {l} {z} {y} {x} {b :: (x, y, z)} {a :: j -> k -> l}. T x y z l k j a b So if :info is to be believed, uniques don't (appear to) have an effect on the order in which the kind variables are bound in the type constructor, but they do have an effect with :type (which isn't surprising, since :type re-generalizes the type signature, and generalization is precisely what you found to be non-deterministic). Ryan S.