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

[GHC]

#15674: GADT's displayed type is misleading
-------------------------------------+-------------------------------------
        Reporter:  AntC              |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.6.1-beta1
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to [comment:3 goldfire]:
 > ... you can say `MkDG2 @Int` while you can't do that with `MkDG`. Their
 types are subtly different.
 >

 Aagh. My brain just blew a fuse.

 > > (And setting `-fprint-explicit-foralls` doesn't explicitly show the
 `forall` in `MkDG`, although it does in `MkDG2`.
 >
 > There is no `forall` in `MkDG`, which doesn't quantify over any
 variables.
 >

 Then I totally ignore the `a` in the `data DG a where ...`? (I don't mean
 its specific variable name, I mean the fact that `MkDG`'s return type is
 more specific that the `data`'s head, which is what makes it a GADT.)

 > > But `MkDG2`'s decl doesn't have an explicit `forall`, neither do I
 need `-XExplicitForAll` to compile it -- that's not implied by `-XGADTs`,
 surprisingly.)
 >
 > Your code does not contain an explicit `forall` in `MkDG2`. It contains
 an implicit one, implied by the presence of the type variable `a`.
 >

 For `MkDG2`, with `-fprint-explicit-foralls`
   `:i` shows `MkDG2 :: forall a. (a ~ Int) => a -> DG a`

   `:t` shows `MkDG2 ::                      Int -> DG Int`

 With `-fno-print-explicit-foralls`
   `:i` shows `MkDG2 ::           (a ~ Int) => a -> DG a`

   `:t` shows `MkDG2 ::                      Int -> DG Int`

 Is that intended behaviour? It doesn't seem either internally consistent,
 nor consistent with your explanation: why is the `forall` appearing at
 all? Why is it appearing for `:i` but not `:t`?

 For `:t`, why is the `(a ~ Int)` not showing, even with verbosity to the
 max? `MkDG2`'s decl does have that explicitly, and it does make a (subtle)
 difference to the type.

 >
 > I'm not sure what `forall`s you're looking for. There isn't one in
 `MkDG`.

 What I'm looking for with these mind-blowingly similar-but- "subtly
 different" nuances is strong help from the compiler to navigate error
 messages when I get my types wrong. (Or rather, when I get wrong the types
 I'm importing from some library whose internals I don't really want to
 tangle with.)

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