[GHC] #11376: Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications

[GHC]

#11376: Inconsistent specified type variables among functions and datatypes/classes
when using -XTypeApplications
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |             Keywords:
      Resolution:                    |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I found another inconsistency with regards to datatypes vs. data families
 and visible type application. Let's define a datatype first:

 {{{
 $ /opt/ghc/head/bin/ghci
 GHCi, version 8.1.20160120: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/xnux/.ghci
 λ> :set -XTypeInType -XTypeApplications
 λ> data T k2 k4 (f :: k1 -> k2 -> k3 -> k4) = T
 λ> :t T
 T :: forall k1 k3 k2 k4 (f :: k1 -> k2 -> k3 -> k4). T k2 k4 f
 λ> :t T @Int
 T @Int :: forall k3 k2 k4 (f :: Int -> k2 -> k3 -> k4). T k2 k4 f
 }}}

 Nothing surprising here. The type variables are topologically sorted such
 that the last three variables correspond to the specified type variables.
 Looks good.

 But if I define the equivalent data family instance, I get a surprisingly
 different result:

 {{{
 λ> :set -XTypeInType -XTypeApplications  -XTypeFamilies
 λ> data family T (a :: k1) (b :: k2) (c :: k3)
 λ> data instance T k2 k4 (f :: k1 -> k2 -> k3 -> k4) = T
 λ> :t T
 T :: forall k2 k4 k1 k3 (f :: k1 -> k2 -> k3 -> k4). T k2 k4 f
 λ> :t T @Int
 T @Int :: forall k4 k1 k3 (f :: k1 -> Int -> k3 -> k4). T Int k4 f
 }}}

 This time, the kind variables are in a completely different order! The
 specified kind variables now come before the invisible kind variables, and
 as a result, `T @Int` has a completely different type.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11376#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler