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 fprintexplicitkinds
[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 fprintexplicitkinds
[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 lefttoright, 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 