GHCi gives conflicting information about visible type application

From the docs for -XVisibleTypeApplication:

When printing types with -fprint-explicit-foralls (page 72) enabled, type variables not available for visible type application are printed in braces. Thus, if you write myLength = length without a type signature, myLength‘s inferred type will be forall {f} {a}. Foldable f => f a -> Int.

> :set -XScopedTypeVariables
> :set -XTypeApplications
> :set -fprint-explicit-foralls
> let foo :: forall a. a; foo = undefined    (LINE 1)
> :t foo
foo :: forall {a}. a                         (LINE 2)
>
> :t (foo @Bool)
(foo @Bool) :: Bool                          (LINE 3)

Type application with foo (LINE 1) should be possible, but GHCi claims it is not (LINE 2), then allows it anyway (LINE 3). This looks like a bug with fprint-explicit-foralls in detecting which variables are available for type application.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	GHCi
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #12601 (closed)

changed weight to 5

added GHCi Tbug Trac import labels

added TypeApplications label

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.

The docs don't show anything for "regeneralize". What does that mean, and why does GHCi do it?

What prompted this is chronicled in #11376 (closed) (particularly from 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 (closed), 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.

Trac metadata

Trac field	Value
Related	- → #11376 (closed), #11975 (closed)

I **really** appreciate your explanation.

I frequently use GHCi to learn about my program, and it's extremely unhelpful when it lies to me (see this for another example.) Therefore it seems like type application visibility information should only be displayed with lazy constraint instantiation, i.e., when the +v option is used. Then there's no convoluted explanation needed, and more importantly, you will always get correct information.

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?

The reason I feel that GHCi is giving me incorrect info is due to the existing documentation that I quoted above. Basically, my understanding is that if foo :: forall {k} . k then GHCi should throw an error if I try to write foo @Int, and if foo :: forall k . k, then GHCi should happily accept foo @Int.

When I see foo :: forall {k} . k, but GHCi also lets me write foo @Int, I have no idea what it means by {k}. This seems like a contradiction. I get the impression from your comments that there's something more subtle going on here that I don't understand. If you think others might have the same misconception as me, I would encourage you to improve the existing docs as well.

In regards to your suggestion, I think it would be good to put a blurb in the Visible Type Application section (9.18 by my count) as well, near the "detail" note that explains the curly braces.

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.

One more point to make about GHCi's lies: when GHCi doesn't lie, outrage ensues. That debate shows that beginners (and, indeed, most Haskellers doing routine Haskelling) can't handle the truth. My point here is that lying is not always undesired behavior.

I've submitted 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?

mentioned in commit b335f506

changed milestone to %8.2.1

added 1 deleted label

closed

Merged to ghc-8.2 in 7596efd6.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added Pnormal label