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

@@ -51,0 +51,3 @@
+
+ EDIT: Most of this is fix, as of March 25. But the data family stuff in
+ comment:12 is still outstanding, and we need a test case.

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.

 EDIT: Most of this is fix, as of March 25. But the data family stuff in
 comment:12 is still outstanding, and we need a test case.

--

Comment (by goldfire):

 Replying to [comment:16 simonpj]:
 > I think the fact that the context doesn't go away is a bug in visible
 type application.  Richard?

 Instantiation is lazy. There's (currently) no incentive for GHC to solve
 that constraint when you say `datatypeName @blah`.

 Consider

 {{{
 foo :: forall a b. Show a => ...
 }}}

 and `foo @Int`. What type should this have? `forall b. Show Int => ...`
 seems the natural choice. The only way to get, say, `forall b. ...`
 (solving the constraint) would be to instantiate and regeneralize, but
 then we'd get `forall {b}. ...`, which is quite silly.

 We could have some logic that looks to see if no specified type variables
 are left at the beginning of the type and then instantiate constraints.
 But I'm not sure this is a good idea. Seems a bit arbitrary. Always being
 lazy seems simpler.

 As for the other problems in this ticket: they're mostly fixed now, except
 for the data family bit.

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