How does topological sorting of kind variables really work?

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


> I thought that inferred foralls are Invisible binders (see Note [TyBinders and VisibilityFlags]); and you can't use visible type application for Invisible binders.

In this particular case, j, k, l, x, y, and z aren't invisible
binders, but rather specified ones. And you certainly can use visible
type application on specified binders; this is important for my use
case.

> Also I don't understand why Ryan needs a reliable ordering.

I guess I should elaborate on what exactly my use case is. I'm trying
to fix Trac #10604 (i.e., make Generic1 poly-kinded). As part of this
effort, I need to generalize the (:.:) type [2] from GHC.Generics like
so:

    newtype (:.:) (f :: k2 -> *) (g :: k1 -> k2) (p :: k1) = Comp1 (f (g a))

I also need to change a part of TcGenGenerics where I apply the (:.:)
type constructor to some other types [3]. Previously, (:.:) was
monokinded, so I only needed to apply (:.:) to some type arguments.
But now that (:.:) is poly-kinded, I need to also apply it to two kind
arguments!

Now for the interesting part: in which order do you give the kind
arguments for (:.:)? I originally thought the order in which you'd do
it would be [k2,k1] (since that's the order they appear in the
definition from left to right), but in reality, it's actually [k1,k2]
due to the reasons mentioned earlier in this thread. This is quite
bewildering, especially since in GHC 7.10.3, it was the former order,
but in GHC 8.0 it's the latter order. Who's to say that the order
won't change again in a later GHC, and then deriving Generic1 will
silently break as a result?

So at this point, I see my options as follows:

1. Change the definition of (:.:) to use the GADT syntax that Richard
proposed. This would give a stable ordering for the kind variables,
but I'm loathe to make such a drastic change to the surface syntax to
fix a silly problem like this.
2. Investigate a fix to the implicitly quantified ordering issue. I'm
not sure where the issue could lie, and just from looking at
extract_lty [4], it's not clear at all what causes the current
ordering.
3. Live with the issue, and just change the code in TcGenGenerics if
the kind variable ordering ever changes. This is a bummer, but looks
like the simplest option.

Ryan S.
-----
[1] https://ghc.haskell.org/trac/ghc/ticket/10604
[2] http://hackage.haskell.org/package/base-4.8.2.0/docs/GHC-Generics.html#t::.:
[3] http://git.haskell.org/ghc.git/blob/d81cdc227cd487659995ddea577214314c9b4b97:/compiler/typecheck/TcGenGenerics.hs#l526
[4] http://git.haskell.org/ghc.git/blob/d81cdc227cd487659995ddea577214314c9b4b97:/compiler/rename/RnTypes.hs#l1611


More information about the ghc-devs mailing list