#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