[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:                    |
-------------------------------------+-------------------------------------

Old description:

> 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 => ()
> }}}

New description:

 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 => ()
 }}}

 EDIT: See also documentation infelicity in comment:9.

--

Comment (by goldfire):

 Replying to [comment:8 rwbarton]:
 > Based on experimentation, the rule seems to be: all type variables
 mentioned in the type signature are explicit, from left to right as they
 appear in the signature. I guess `k` counts as to the left of `a` in `a ::
 k`, though, since it is implicitly quantified earlier.

 Here are the rules:
 * All variables mentioned by name are specified.
 * To get the ordering, list all the variables ordered left-to-right by
 first occurrence. Then do a stable topological sort based on dependencies.

 The second bullet is why `k` goes before `a` even though `a` is mentioned
 first. There is a note about this in the manual, but it doesn't discuss
 the topological sort part. Will fix.

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