[GHC] #13524: GHC does not preserve order of forall'd vars with TypeApplications

[GHC]

#13524: GHC does not preserve order of forall'd vars with TypeApplications
-------------------------------------+-------------------------------------
           Reporter:  crockeea       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code compiles with 8.0.2. Note that the order of variables
 on `pt1` is `a :: *` and `expr :: * -> *`, and this is the order of the
 type application in `main`.

 {{{
 {-# LANGUAGE PartialTypeSignatures #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeApplications      #-}

 {-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}

 type Empty a = ()

 foo :: expr a -> expr a -> expr (Empty a)
 foo = undefined

 newtype Expr a = SPT {run :: String}

 pt1 :: forall a ptexpr . ptexpr a -> ptexpr (Empty a)
 --pt1 :: forall a ptexpr . ptexpr a -> ptexpr _
 pt1 a = foo a a

 main :: IO ()
 main = putStrLn $ run $ pt1 @Int @Expr undefined
 }}}

 If I use partial type signatures with the alternate signature for `pt1`
 (which has the same order of the `forall`), I get these errors:


 {{{
 Bug.hs:19:25: error:
     • Couldn't match type ‘Int’ with ‘Expr’
       Expected type: Expr (Empty Expr)
         Actual type: Int (Empty Expr)
     • In the second argument of ‘($)’, namely
         ‘pt1 @Int @Expr undefined’
       In the second argument of ‘($)’, namely
         ‘run $ pt1 @Int @Expr undefined’
       In the expression: putStrLn $ run $ pt1 @Int @Expr undefined

 Bug.hs:19:30: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the type ‘Int’
       In the second argument of ‘($)’, namely ‘pt1 @Int @Expr undefined’
       In the second argument of ‘($)’, namely
         ‘run $ pt1 @Int @Expr undefined’

 Bug.hs:19:35: error:
     • Expecting one more argument to ‘Expr’
       Expected a type, but ‘Expr’ has kind ‘* -> *’
     • In the type ‘Expr’
       In the second argument of ‘($)’, namely ‘pt1 @Int @Expr undefined’
       In the second argument of ‘($)’, namely
         ‘run $ pt1 @Int @Expr undefined’
 }}}

 The errors are saying that the kinds of the type applications are
 incorrect, but nothing in the order of `pt1`s `forall` nor the order of
 application has changed.

 However, if I then change the order of the type applications in `main` to
 `main = putStrLn $ run $ pt1 @Expr @Int undefined`, GHC accepts the
 program, even though the kinds of types in the application are incorrect
 with respect to the order listed in `pt1` (so it should reject the
 program).

 Somehow GHC has swapped the order of `a` and `ptexpr` in the variable list
 for `pt1`.

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