[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:  8.0.1
       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):

 What about for data constructors?

 Without your patch:
 {{{
 > :type Proxy
 Proxy :: forall {k} (t :: k). Proxy t
 }}}

 This is now useful information that `k` is not specified but `t` is.

 With your patch (assumedly -- I don't have this locally):
 {{{
 > :type Proxy
 Proxy :: forall {k} {t :: k}. Proxy t
 }}}

 I now don't know which is specified and which is generalized.

 So I could use `:info`:

 {{{
 > :info Proxy
 type role Proxy phantom
 data Proxy (t :: k) = Proxy
         -- Defined in ‘Data.Proxy’
 instance forall k (s :: k). Bounded (Proxy s)
   -- Defined in ‘Data.Proxy’
 instance forall k (s :: k). Enum (Proxy s)
   -- Defined in ‘Data.Proxy’
 instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’
 instance Monad Proxy -- Defined in ‘Data.Proxy’
 instance Functor Proxy -- Defined in ‘Data.Proxy’
 instance forall k (s :: k). Ord (Proxy s)
   -- Defined in ‘Data.Proxy’
 instance forall k (s :: k). Read (Proxy s)
   -- Defined in ‘Data.Proxy’
 instance forall k (s :: k). Show (Proxy s)
   -- Defined in ‘Data.Proxy’
 instance Applicative Proxy -- Defined in ‘Data.Proxy’
 instance Foldable Proxy -- Defined in ‘Data.Foldable’
 instance Traversable Proxy -- Defined in ‘Data.Traversable’
 instance forall k (s :: k). Monoid (Proxy s)
   -- Defined in ‘Data.Proxy’
 }}}

 There's an awful lot of information I have no interest in, and the very
 piece of information I do want -- the specificity of the variables -- is
 missing. It's missing because GHC helpfully says `data Proxy (t :: k) =
 ...` even though `Data.Proxy` declares `data Proxy t = ...`. The former
 would make `k` specified. But the latter, actual definition, means that
 `k` is not specified.

 I can exhibit the same problems with a class method. Take
 `Control.Category`'s `id`:

 Without your patch:
 {{{
 > :type C.id
 C.id
   :: forall {k} (cat :: k -> k -> *).
      Category cat =>
      forall (a :: k). cat a a
 }}}
 Very helpful info.

 With your patch (assumedly):
 {{{
 > :type C.id
 C.id
   :: forall {k} {a :: k} {cat :: k -> k -> *}.
      Category cat => cat a a
 }}}
 Here I decided to swap the order of `cat` and `a`, because it's quite
 conceivable that this would happen.

 And now `:info`:
 {{{
 > :info C.id
 class Category (cat :: k -> k -> *) where
   Control.Category.id :: forall (a :: k). cat a a
   ...
 }}}
 Once again, I can't tell that `k` is unspecified. And even if I could
 somehow, I'd still have to do some work to reconstruct the type from this
 information.

 I'm sure record selectors would have the same problem.

 Bottom line: I don't think Simon's proposal to use `:info` for bare names
 quite does it. I'm sympathetic to disliking (1) and I, too, desire to keep
 things simple. But I don't think we've quite figured this out yet.

 I actually think there's a really easy solution: have `:type` print
 ''both'' the uninstantiated type and the instantiated one (if they're
 different, by more than the ordering of invisible things). `tcRnExpr`
 could return two `Type`s -- it has both types we want to hand. We could
 even only do this new behavior when `-fprint-explicit-foralls` is enabled
 (because otherwise, the user isn't seeing specificity anyway).

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