Opened 7 months ago

Closed 6 months ago

#13401 closed bug (fixed)

GHCi gives conflicting information about visible type application

Reported by: crockeea Owned by:
Priority: normal Milestone: 8.2.1
Component: GHCi Version: 8.0.1
Keywords: TypeApplications Cc:
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:

Description

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.

Change History (13)

comment:1 Changed 7 months ago by simonpj

Keywords: TypeApplications added

comment:2 Changed 7 months ago 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.

comment:3 Changed 7 months ago by crockeea

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

comment:4 Changed 7 months ago by RyanGlScott

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

comment:5 Changed 7 months ago by crockeea

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.

comment:6 Changed 7 months ago 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?

comment:7 Changed 7 months ago by crockeea

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.

comment:8 Changed 7 months ago 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.

comment:9 Changed 7 months ago by goldfire

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.

comment:10 Changed 7 months ago by RyanGlScott

Differential Rev(s): Phab:3310
Status: newpatch

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?

comment:11 Changed 6 months ago by Ryan Scott <ryan.gl.scott@…>

In b335f50/ghc:

Further document :type +v's role in analyzing -XTypeApplications in GHCi

Summary:
The section on `-XTypeApplications` in the users' guide isn't terribly
clear on how to view the visibility of a function type signature's type
variables in GHCi properly (i.e., using the `:type +v` GHCi command). This
adds some more exposition that demonstrates how to use `:type +v` (and why you
don't want to use `:type`).

Fixes #13401.

Test Plan: Eyeball it

Reviewers: bgamari, austin, goldfire, crockeea

Reviewed By: goldfire, crockeea

Subscribers: rwbarton, thomie, crockeea

Differential Revision: https://phabricator.haskell.org/D3310

comment:12 Changed 6 months ago by RyanGlScott

Milestone: 8.2.1
Status: patchmerge

comment:13 Changed 6 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.