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

 Replying to [comment:5 AntC]:
 > > 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 ...`?

 In GADT syntax, the bit between the `data` and the `where` is the
 declaration for the type only -- not any constructors. The `a` there
 serves to say that `DG` takes one argument. It does not affect or cause
 any variable quantification in constructors.

 >
 > 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`?

 Yes, this is all expected behavior. Haskell allows you omit `forall`s if
 you have a type variable in a type. But when you write `-fprint-explicit-
 foralls`, it will print one even if you left it out. So: the `forall`
 appears because you asked for it.

 I'll quote myself:

 > `:type <expr>` gives you the type that is assigned to it if you had `let
 it = <expr>`. It's a uniform rule that always works.

 When we say `let it = MkDG2`, GHC instantiates the type of `MkDG2` at its
 occurrence and then generalizes (because `let`-bound variables are
 generalized). Thus, `it` might not have exactly the same type as `MkDG2`,
 which is what's happening here.

 Here's a simpler example:

 {{{#!hs
 silly :: (Ord a, Eq a) => a -> Bool
 silly = ...
 }}}

 Asking for `:t silly` gives you `Ord a => a -> Bool`. This is because we
 instantiate and regeneralize the type of `silly`. In this process, GHC
 realizes that `Eq a` is redundant and drops it. The same is happening with
 `MkDG2`.


 > 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.

 Short of a use of a type application (which doesn't seem to be what you're
 doing), `MkDG` and `MkDG2` behave identically.

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