# How does topological sorting of kind variables really work?

Ryan Scott ryan.gl.scott at gmail.com
Wed Apr 13 17:30:15 UTC 2016

```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
λ> 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
λ> 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.
```