[GHC] #15674: GADT's displayed type is misleading

[GHC]

#15674: GADT's displayed type is misleading
-------------------------------------+-------------------------------------
           Reporter:  AntC           |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1-beta1
           Keywords:                 |  Operating System:  Windows
       Architecture:  x86_64         |   Type of failure:  Poor/confusing
  (amd64)                            |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHCi's `:t` alleges these three data constructors have the same type `::
 Int -> T Int` (modulo name of the type constructor):

 {{{#!hs
 data DG a where MkDG  ::            Int -> DG Int
                 MkDG2 :: (a ~ Int) => a -> DG a

 data family DF a
 data instance DF Int where MkDF ::  Int -> DF Int
 }}}

 I tried switching on verbosity flags, but to no avail: `-fprint-explicit-
 foralls, -fprint-equality-relations`, and a few others.

 The `DG` constructors are GADTs, the `DF` constructor is not. So it's not
 hard to see different type-level behaviour:

 {{{#!hs
 f (MkDF  x) = x                   -- accepted without a signature
 -- f :: DF Int -> Int             -- inferred signature, or you can spec
 it
 -- f :: DF a   -> a               -- rejected: signature is too general/
                                   -- a is a rigid type variable

 g (MkDG  x) = x                   -- } without a signature, rejected
 g (MkDG2 x) = x                   -- } "untouchable" type (Note)

 -- g :: DG Int -> Int             -- } g accepted with either sig
 -- g :: DG a   -> a               -- } ?but MkDG doesn't return DG a,
 allegedly
 }}}

 '''Note:''' at least the error message re `MkDG2` does show its type as
 `:: (forall a). (a ~ Int) => DG a -> a`. But doggedly `MkDG :: Int -> DG
 Int`.

 "Untouchable" error messages are a fertile source of questions on
 StackOverflow. The message does say `Possible fix: add a type signature
 for 'g'`, but gives no clue what the signature might be.

 If you've imported these data constructors from a library, such that you
 can't (easily) see they're GADTs, couldn't `:t` give you better help to
 show what's going on? Or should one of the verbosity flags already do
 this?

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