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

Comment (by goldfire):

 But this would lead to confusing behavior if there are any uninstantiated
 specified variables. If we did instantiation, then `:t f` would answer
 `Int -> Int -> Int`. That's reasonable enough, but then it's quite
 surprising when `:t f @Int` is accepted! In a somewhat similar scenario,
 say `bar :: forall a b. Show a => a -> b -> a`. What should `:t bar @Int`
 say? I offer 4 choices:

 1. `forall b. Show Int => Int -> b -> Int`
 2. `forall b. Int -> b -> Int`
 3. `forall {b}. Int -> b -> Int`
 4. `Int -> b -> Int`

 Here is how these could be produced:
 1. This is what is currently done. No instantiation at `:type`.
 2. This would require some new algorithm that instantiates a type and
 regeneralizes, being very careful to somehow notice when the instantiated
 variable arose from a specified variable and mark the re-generalized
 variable as specified. This becomes quite hard (both to implement and to
 specify) when equality constraints are in the mix and might combine a
 specified variable with an invisible one.
 3. Instantiate and regeneralize. But now it looks like `bar @Int @Bool`
 should be rejected, even though it's actually OK.
 4. Instantiate and do not regeneralize. Here, the user can't know that
 `bar @Int @Bool` is OK, but at least we're not suggesting that it should
 be rejected.

 As you can see, I prefer (1). It's conceivable to make a different choice
 when there are no top-level specified variables (so that a further type
 parameter would be an error), but I don't think we should. (Before arguing
 against me here, consider `quux :: forall a. Int -> forall b. Show a => b
 -> a -> Bool`. What should `:type quux @Int` say?)

 Another option I'd be happy with: Option (1) when `-fprint-explicit-
 foralls` is on, and option (3) when it's not. This might be surprising to
 users, but the benefits may outweigh the costs.

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