[GHC] #15674: GADT's displayed type is misleading
#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
#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 simonpj): `:type <expr>` tells you the type of the expression `<expr>`, where `<expr>` can be any old expression, not just a single identifier. On the other hand `:info <name>` gives you information about the declaration of the entity `<name>`. And indeed `:info MkDF`, `:info MkDG` and `:info MkDG2` give you the info that I think you want. This works if the constructors are imported from a library that you can't (easily) see. Does that help? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15674#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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:1 simonpj]: Thank you Simon.
`:type <expr>` tells you the type of the expression `<expr>`, where `<expr>` can be any old expression, not just a single identifier.
Yes. So you're saying those three data constructors are at the same type, considered as expressions(?) What is it about their typedness that explains the observable difference in behaviour wrt the functions? (It's to do with pattern matching/deconstructing, rather than applying them as functions/constructing.)
On the other hand `:info <name>` gives you information about the declaration of the entity `<name>`.
Yes, `:info` more or less shows the code that declares `<name>`.
And indeed `:info MkDF`, `:info MkDG` and `:info MkDG2` give you the info that I think you want.
Hmm. `:info` still shows `MkDF :: Int -> DF Int`, `MkDG :: Int -> DG Int`. It does show `MkDG2 :: (a ~ Int) => a -> DG a` or even `MkDG2 :: forall a. (a ~ Int) => a -> DG a`. So ''prima facie'' `MkDF, MkDG`'s types are the same; `MkDG2`'s is different. But actually `MkDG` is the same as `MkDG2`. (And setting `-fprint-explicit-foralls` doesn't explicitly show the `forall` in `MkDG`, although it does in `MkDG2`. 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.)
This works if the constructors are imported from a library that you can't (easily) see.
Does that help?
Perhaps `:t` should behave precisely like `:i` if it is given a single identifier as its argument. That would be non-uniform and ad-hoc, but
Ok. perhaps useful in practice. Usually if I'm having trouble from error messages to do with "untouchable" or "rigid", it's `:t` I go to. I just have to kick myself to go to `:i`. But even the type signature showing in `:i` is misleading. Perhaps: if `<name>` is a data constructor, and not a H98 constructor, and `-fprint- explicit-foralls` is set, show the foralls explicitly? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15674#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
(It's to do with pattern matching/deconstructing, rather than applying
#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:2 AntC]: them as functions/constructing.) Precisely.
So ''prima facie'' `MkDF, MkDG`'s types are the same; `MkDG2`'s is different.
This is true.
But actually `MkDG` is the same as `MkDG2`.
In most contexts, yes. But you can say `MkDG2 @Int` while you can't do that with `MkDG`. Their types are subtly different.
(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.
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.)
Does that help?
Perhaps `:t` should behave precisely like `:i` if it is given a single identifier as its argument. That would be non-uniform and ad-hoc, but
Your code does not contain an explicit `forall` in `MkDG2`. It contains an implicit one, implied by the presence of the type variable `a`. perhaps useful in practice. But that would be non-uniform and ad-hoc. :) `: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.
Usually if I'm having trouble from error messages to do with
"untouchable" or "rigid", it's `:t` I go to. I just have to kick myself to go to `:i`. But even the type signature showing in `:i` is misleading. Perhaps: if `<name>` is a data constructor, and not a H98 constructor, and `-fprint-explicit-foralls` is set, show the foralls explicitly? I'm not sure what `forall`s you're looking for. There isn't one in `MkDG`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15674#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 monoidal): One way to see the difference is to define {{{ pattern PDG a = MkDG a pattern PDG2 a = MkDG2 a pattern PDF a = MkDF a }}} then `:i PDG PDG2 PDF` will show {{{ pattern PDG :: () => (a ~ Int) => Int -> DG a -- Defined at GA.hs:8:1 pattern PDG2 :: () => (a ~ Int) => a -> DG a -- Defined at GA.hs:9:1 pattern PDF :: Int -> DF Int -- Defined at GA.hs:10:1 }}} Should we show this and how? I don't know. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15674#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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:4 monoidal]: Thank you for the tip with defining patterns. It's the only way to reveal the differences here: {{{#!hs data family DG3 a data instance DG3 a where MkDG3 :: Int -> DG3 [Int] data family DG4 a data instance DG4 [a] where MkDG4 :: Int -> DG4 [Int]
:i PDG3 PDG4
pattern PDG3 :: () => (a ~ [Int]) => Int -> DG3 a pattern PDG4 :: () => (a ~ Int) => Int -> DG4 [a] }}}
Should we show this and how? I don't know.
Now we have variable `a` showing. But according to Richard's message, it shouldn't be because it's not `forall`'d, neither explicitly nor implicitly (sigh). And indeed `:i` for the data constructors doesn't show `(a ~ ...)` even with full verbosity. My understanding of pattern synonyms is that they're built on top of data constructors. Then it seems back-to-front to use pattern synonyms to diagnose constructors. This ticket arose from a quest to understand `data` and `data instance`s from the ground up. I can't find any firm ground to start from, only quicksand. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15674#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Phyx-): * os: Windows => Unknown/Multiple * architecture: x86_64 (amd64) => Unknown/Multiple Comment: Not a Windows specific issue, reclassifying. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15674#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC