[GHC] #15568: Kind variables in type family aren't quantified in toposorted order

25 Aug 2018

      #15568: Kind variables in type family aren't quantified in toposorted order
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications, TypeFamilies     |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Recently, I noticed that an error message I was experiencing differs
 between GHC 8.4.3 and GHC 8.6.1+. Take this program:

 {{{#!hs
 {-# 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15568
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler