#13401: GHCi gives conflicting information about visible type application -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): What is happening here is that `:type` is regeneralizing the type of the expression `foo`. In the regeneralized type, `a` is now properly invisible (i.e., not available for type application), which is why `:type foo` will give you `forall {a}. a` regardless of whether you declared foo with `foo = undefined` or `foo :: a; foo = undefined`. If you wish to see the type of `foo` that preserves the visibility of its type parameters, you need to use the `:type +v` GHCi command (which is currently only available in GHC HEAD): {{{ λ> let foo = undefined λ> :type +v foo foo :: forall {a}. a λ> let foo :: a; foo = undefined λ> :type +v foo foo :: forall a. a }}} So I don't think there's a GHC bug here—just slightly misleading documentation at worst. I think including a mention of `:type +v` in the users' guide section on `-XTypeApplications` might dispel this confusion. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13401#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13401: GHCi gives conflicting information about visible type application -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11376, #11975 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #11376, #11975 Comment: What prompted this is chronicled in #11376 (particularly from [https://ghc.haskell.org/trac/ghc/ticket/11376#comment:15 comment:15] onward). It was discovered that when `:type` was used with a visibly applied type, you could get some weird results, like this one: {{{ λ> import GHC.Generics λ> :type datatypeName @('MetaData "Void" "Data.Void" "base" 'False) datatypeName @('MetaData "Void" "Data.Void" "base" 'False) :: Datatype ('MetaData "Void" "Data.Void" "base" 'False) => forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *) (a :: k1). t ('MetaData "Void" "Data.Void" "base" 'False) f a -> [Char] }}} Before, `:type` was instantiating constraints lazily, which is why that `Datatype` constraint is still lingering around in the type that `:type` infers above, even though `'MetaData "Void" "Data.Void" "base" 'False` should discharge that constraint. simonpj thought this was ghastly and changed the behavior of `:type` to //deeply// instantiate the inferred type (i.e., solve constraints as much as possible) and re-generalize afterwards. (Note: "generalize" comes from a rule in Hindley–Milner type inference, I believe, where you infer a type of the form `forall a. ...`). After this change, you get this instead: {{{ λ> :type datatypeName @('MetaData "Void" "Data.Void" "base" 'False) datatypeName @('MetaData "Void" "Data.Void" "base" 'False) :: t ('MetaData "Void" "Data.Void" "base" 'False) f a -> [Char] }}} which is certainly nicer to look at. But it comes at a downside: deep instantiation followed by re-generalization can change the visibilities of type parameters, which explains the behavior you reported originally in this ticket. To work around this, goldfire introduced `:type +v` in #11975, which gives you the original lazy instantiation behavior that `:type` used to have. OK, that ended being a much lengthier explanation that I'd hoped for. Hopefully, you understand the context of this a little better. My question to you is now: how should we update the users' guide to explain this wrinkle? I'm a bit reluctant to include a crash-course on HM type inference, but maybe there's an instructive way to give the highlights of this discussion to readers. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13401#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13401: GHCi gives conflicting information about visible type application -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11376, #11975 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): It's not that the information that `:type` gives is wrong, it's just not what you're asking for. `:type foo` gives you the visibility of `foo` as an expression post-typechecking. This can be quite handy when you have, say: {{{ λ> let foo :: a; foo = undefined λ> :type foo @Int foo @Int :: Int λ> :type foo foo :: forall {a}. a λ> let goo = foo λ> :type goo goo :: forall {a}. a λ> :type goo @Int }}} Notice that you can't use VTA with `goo`, since its type (which is the same as `foo`, post-typechecking) doesn't have any visible type variables. This is precisely what `:type foo` warned us about, and I'd hate to cripple a legitimately useful feature for the benefit of a degenerate case. My suggestion would be to include a blurb in the users' guide section that gives an example of asking GHCi for the visibility of a top-level expression (using `:type +v`), and then show the pitfalls of using `:type`. Would you be satisfied with that? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13401#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13401: GHCi gives conflicting information about visible type application -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11376, #11975 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree with Ryan's explanations. `:type expr` gives you the type that would be assigned to `x` if you say `let x = expr`. `:type +v expr` gives you the type of `expr`. One challenge here is that `foo` ''does'' have type `forall {k}. k`. It also has type `forall k. k`. It also has type `Int`. One challenge in a type system like Haskell's is that an expression has many types. All this said, I do agree with @crockeea's suggestions to clarify the documentation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13401#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13401: GHCi gives conflicting information about visible type application -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: GHCi | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11376, #11975 | Differential Rev(s): Phab:3310 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:3310 Comment: I've submitted Phab:D3310, which attempts to spruce up the documentation pertaining to this section of the users' guide. crockeea, goldfire, do you mind giving it a read and seeing if it makes sense? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13401#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13401: GHCi gives conflicting information about visible type application -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.2.1 Component: GHCi | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11376, #11975 | Differential Rev(s): Phab:3310 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => merge * milestone: => 8.2.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13401#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler