Kind variables in type family aren't quantified in toposorted order

Recently, I noticed that an error message I was experiencing differs between GHC 8.4.3 and GHC 8.6.1+. Take this program:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Proxy
import GHC.Exts (Any)

type family F (a :: j) :: k

f :: Proxy a -> Proxy (F (a :: j) :: k)
f _ = Proxy :: Proxy (Any :: k)

On 8.4.3, you'll get:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:7: error:
    • Couldn't match type ‘Any k’ with ‘F j k a’
      Expected type: Proxy k (F j k a)
        Actual type: Proxy k (Any k)
    • In the expression: Proxy :: Proxy (Any :: k)
      In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)
    • Relevant bindings include
        f :: Proxy j a -> Proxy k (F j k a) (bound at Bug.hs:11:1)
   |
11 | f _ = Proxy :: Proxy (Any :: k)
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^

But on 8.6.1 and HEAD, you'll instead get:

$ /opt/ghc/8.6.1/bin/ghc Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:7: error:
    • Couldn't match type ‘Any k’ with ‘F k j a’
      Expected type: Proxy k (F k j a)
        Actual type: Proxy k (Any k)
    • In the expression: Proxy :: Proxy (Any :: k)
      In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)
    • Relevant bindings include
        f :: Proxy j a -> Proxy k (F k j a) (bound at Bug.hs:11:1)
   |
11 | f _ = Proxy :: Proxy (Any :: k)
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^

Notice that on 8.4.3, it displays F j k a, but on 8.6.1, it displays F k j a! After some digging, it turns out that this is because on 8.6.1, the order of F's kind variables are quantified completely differently! On 8.4.3, we have:

λ> :kind F
F :: forall j k. j -> k

But on 8.6.1, we have:

λ> :kind F
F :: forall k j. j -> k

I would prefer the old behavior of 8.4.3, since j k is what you get after performing a left-to-right, reverse topological sort on the kind variables of F, which is consistent with how type signatures quantify their type variables. Currently, this quirk doesn't matter that much (except for error messages, as shown above), but if/when visible kind application is implemented, it'll be more noticeable.

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture