[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:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Other
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Originally reported [https://mail.haskell.org/pipermail/ghc-
 devs/2016-January/010915.html here]. When applying types via
 `-XTypeApplications`, the type/kind that gets instantiated seems to be
 different depending on whether you're using functions, datatypes, or
 typeclasses.

 Here's an example contrasting functions and datatypes:

 {{{
 $ /opt/ghc/head/bin/ghci
 GHCi, version 8.1.20160106: http://www.haskell.org/ghc/  :? for help
 λ> :set -fprint-explicit-kinds -XTypeApplications -XTypeInType
 λ> data Prox a = Prox
 λ> prox :: Prox a; prox = Prox
 λ> :t prox
 prox :: forall k (a :: k). Prox k a
 λ> :t prox @Int
 prox @Int :: Prox * Int
 λ> :t Prox
 Prox :: forall k (a :: k). Prox k a
 λ> :t Prox @Int
 Prox @Int :: Prox Int a
 }}}

 This is the core of the problem: with a function, `Int` seems to be
 applied to type variable `a`, whereas with data types, `Int` appears to be
 applied to the kind variable `k`. This confuses me, since `k` wasn't
 specified anywhere in the definition of `Prox`.

 Andres Löh also [https://mail.haskell.org/pipermail/ghc-
 devs/2016-January/010916.html observed] a similar discrepancy between
 functions and typeclasses:

 {{{
 λ> :set -XScopedTypeVariables
 λ> class C a where c :: ()
 λ> d :: forall a. C a => (); d = c @_ @a
 λ> :t d
 d :: forall k (a :: k). C k a => ()
 λ> :t d @Int
 d @Int :: C * Int => ()
 λ> :t c
 c :: forall k (a :: k). C k a => ()
 λ> :t c @Int
 c @Int :: C Int a => ()
 λ> :t c @_ @Int
 c @_ @Int :: C * Int => ()
 }}}

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