[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
      Resolution:                    |             Keywords:
                                     |  TypeApplications
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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I think there's a bit of confusion here. The issue is not that wildcards
 are being treated as visible type variables, as evidenced in this GHCi
 session:

 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive
 GHCi, version 8.3.20170329: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 λ> :set -fprint-explicit-foralls -XPartialTypeSignatures
 λ> let foo :: _ -> b; foo _ = undefined

 <interactive>:2:12: warning: [-Wpartial-type-signatures]
     • Found type wildcard ‘_’ standing for ‘w’
       Where: ‘w’ is a rigid type variable bound by
                the inferred type of foo :: w -> b at <interactive>:2:20-36
     • In the type signature: foo :: _ -> b
 λ> :type +v foo
 foo :: forall {w} b. w -> b
 }}}

 The fresh type variable that gets used in place of `_` is implicitly
 quantified and unspecified, so it is not available for visible type
 application in the first place:

 {{{
 λ> :set -XTypeApplications
 λ> :type +v foo @Int
 foo @Int :: forall {w}. w -> Int
 λ> :type +v foo @Int @Char

 <interactive>:1:1: error:
     • Cannot apply expression of type ‘w0 -> Int’
       to a visible type argument ‘Char’
     • In the expression: foo @Int @Char
 }}}

 This part is working as expected. The issue is the order in which the
 //explicitly// quantified type variables are being returned in the
 presence of `PartialTypeSignatures`. If you take this code

 {{{#!hs
 {-# 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 _
 pt1 a = foo a a
 }}}

 and load it into GHCi, you can see for yourself the exact (incorrect)
 order in which `pt1`'s type variables are appearing:

 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
 GHCi, version 8.3.20170329: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )
 Ok, modules loaded: Main.
 λ> :set -fprint-explicit-foralls
 λ> :type +v pt1
 pt1 :: forall (ptexpr :: * -> *) a. ptexpr a -> ptexpr (Empty a)
 }}}

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