Opened 7 years ago

Closed 2 years ago

Last modified 2 years ago

#4426 closed feature request (fixed)

Simplify the rules for implicit quantification

Reported by: simonpj Owned by: bgamari
Priority: highest Milestone: 8.0.1
Component: Compiler Version: 6.12.3
Keywords: Cc: fischer@…, id@…, ghc.haskell.org@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #7880 Differential Rev(s): Phab:D211, Phab:D1615
Wiki Page:

Description

This thread http://www.haskell.org/pipermail/glasgow-haskell-users/2010-October/019360.html convinced me that GHC's rules for implicit quantification are unnecessarily complicated.


The current spec

The current spec seems to be this:

  • Define an "implicit quantification point" to be (a) the type in a type signature f :: type if type does not start with forall; or (b) a type of form (context => type), that is not immediately enclosed by an explicit forall
  • At each implicit quantification point 'ty', working outside in, GHC finds all the type variables a,b,c in 'ty' that are not already in scope, and transforms 'ty' to (forall a,b,c. ty).

Note that

  • The argument of a constructor is not an implicit quantification point, so that
    data Foo = MkFoo (a -> a)
    
    is an error, and does not mean
    data Foo = MkFoo (forall a. a->a)
    
  • Implicit quantification points may be nested but the inner ones are effectively no-ops. Example
    f :: Int -> (Eq a => a -> a) -> Int
    
    There are two quantification points: the whole type, and the (Eq a => ...). But when the outer quantification point wraps forall a around it, the inner quantification point has no free variables to quantify. So we get
    f :: forall a. Int -> (Eq a => a -> a) -> Int
    

The new proposal

The proposed new rule is this:

  • Implicit quantification applies only to an entire user type signature that does not start with forall.
  • For such signatures, find all the type variables a,b,c in the signature that are not already in scope, and prefix the signature with forall a,b,c.

I believe that the only observable changes in behaviour would be

  • In a data type declaration
    data Foo = MkFoo (Eq a => a -> a)
    
    you'd get an error "a is not in scope", just as you would with
    data Foo = MkFoo (a->a)
    
    To me this seems more consistent behavour.
  • Inside an explicit forall you would get no implicit foralls:
    f :: forall a. (Eq b => b->b) -> a -> a
    
    would yield "b is not in scope", whereas at present it behaves like
    f :: forall a. (forall b. Eq b => b->b) -> a -> a
    

Attachments (7)

0001-Add-fwarn-context-quantification-4426.patch (16.9 KB) - added by monoidal 4 years ago.
Compiler
0001-Test-4426.patch (2.8 KB) - added by monoidal 4 years ago.
Test
0001-Support-for-quantification-on-contexts-GHC-Trac-4426.patch (2.9 KB) - added by monoidal 4 years ago.
Haddock
0001-Add-fwarn-context-quantification-4426.2.patch (16.9 KB) - added by monoidal 4 years ago.
Compiler
ghc.patch (21.7 KB) - added by monoidal 4 years ago.
haddock.patch (2.9 KB) - added by monoidal 4 years ago.
haskeline.patch (966 bytes) - added by monoidal 4 years ago.

Download all attachments as: .zip

Change History (38)

comment:1 Changed 7 years ago by sebf

Cc: fischer@… added

comment:2 Changed 7 years ago by isaacdupree

Cc: id@… added

comment:3 Changed 7 years ago by igloo

Milestone: 7.2.1

comment:4 Changed 6 years ago by igloo

Milestone: 7.4.17.6.1
Priority: normallow

comment:5 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:6 Changed 4 years ago by monoidal

difficulty: Unknown

See also comments at #7880. This change is not hard (I had a very rough sketch that detected ~4 missing quantifier errors in GHC tree) but it's too late for 7.8. Maybe I'll do it such that 7.10 will give a warning and 7.12 an error.

comment:7 Changed 4 years ago by simonpj

Great, thank you!

Simon

comment:8 Changed 4 years ago by Krzysztof Gogolewski <krz.gogolewski@…>

In c4ffdbad3d40887b9b1e8287c90966649ea8571f/ghc:

Fix manual regarding current state of implicit quantification

See also #4426

Changed 4 years ago by monoidal

Compiler

Changed 4 years ago by monoidal

Attachment: 0001-Test-4426.patch added

Test

comment:9 Changed 4 years ago by monoidal

Status: newpatch

Patch attached.

It adds a new warning -fwarn-context-quantification that reports when a variable is quantified only because it under a "=>" arrow. Later, as the proposal says, this warning will be made an out-of-scope error.

Normally, HsForAll is either HsForAll Implicit or HsForAll Explicit, and a context T => R inserts HsForAll Implicit. This patch adds a new value, HsForAll Qualified, which is completely equivalent to HsForAll Implicit save for the warning message. Later, its behavior will be changed and the renamer will not do implicit quantification for variables under HsForAll Quantified.

I made -Wall not imply this flag, in (doubtful) case there is still time to merge this to GHC 7.8. In this case, there is full backwards compatibility: no change in behavior except if the flag is explicitly supplied. However, the API is slightly changed and I had to make a tiny change to Haddock. If it's too late, in GHC 7.10 I'd like -Wall to enable -fwarn-context-quantification, so I'll amend the patch.

Changed 4 years ago by monoidal

Compiler

comment:10 Changed 4 years ago by monoidal

Patch updated for current HEAD.

Changed 4 years ago by monoidal

Attachment: ghc.patch added

Changed 4 years ago by monoidal

Attachment: haddock.patch added

Changed 4 years ago by monoidal

Attachment: haskeline.patch added

comment:11 Changed 4 years ago by monoidal

Milestone: 7.6.27.10.1

I've updated the patches again - three above files are ready for GHC 7.10.

The warning is enabled by default, and the plan is that GHC 7.12 will give an error with implicit quantification on contexts.

comment:12 in reply to:  11 Changed 4 years ago by hvr

Replying to monoidal:

I've updated the patches again - three above files are ready for GHC 7.10.

The patch for hackage:haskeline would have to go via https://github.com/judah/haskeline though...

comment:13 Changed 3 years ago by thoughtpolice

Status: patchinfoneeded

@monoidal: What's the status here? Would you like to merge these patches yourself and get the changed merged to Judah's repository for this to land?

comment:14 Changed 3 years ago by monoidal

Differential Rev(s): Phab:D211
Status: infoneededpatch

The patch (ghc+haddock) is ready for review in Phabricator, and the change to haskeline was merged.

There are only minor changes since the previous patch - I've clarified the documentation and updated TH testcases that were created in the meantime.

comment:15 Changed 3 years ago by Edward Z. Yang <ezyang@…>

In 275dcafbfb6b371dd5d8943fa4df9c23e68f6165/ghc:

Add -fwarn-context-quantification (#4426)

Summary:
This warning (enabled by default) reports places where a context
implicitly binds a type variable, for example

type T a = {-forall m.-} Monad m => a -> m a

Also update Haddock submodule.

Test Plan: validate

Reviewers: hvr, goldfire, simonpj, austin

Reviewed By: austin

Subscribers: simonmar, ezyang, carter

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

GHC Trac Issues: #4426

comment:16 Changed 3 years ago by ezyang

Resolution: fixed
Status: patchclosed

comment:17 Changed 3 years ago by simonpj

Priority: lowhighest
Resolution: fixed
Status: closednew

No, now, let's not close this. There's a pending change for 7.12, namely

  • making the warnings into an error.
  • getting rid of the Qualified constructor in HsExplicitFlag (we can use Explicit instead)
  • remove or deprecate fwarn-context-quantification (I suppose it should be deprecated until 7.14, sigh.)

7.12 isn't a milestone yet (Austin can you fix that?), so I'll milestone it for 7.10 so it doesn't get lost. I'll give it "highest" priority not because it's terribly vital but because it's easy and it'd be untidy to let it linger.

Simon

comment:18 Changed 3 years ago by goldfire

I'm very late to this conversation, so please ignore me if this is silly.

Why not just jump the gun and make this an error right now? Has anyone tried to see how many packages on Hackage this would break? Spreading the effects of this change over 3 releases (warning in 7.10, error in 7.12 while deprecating the warning flag, remove warning flag in 7.14) seems like a lot of overhead when the amount of affected code is (in my uneducated guess) very small.

comment:19 Changed 3 years ago by hvr

Milestone: 7.10.17.12.1

comment:20 Changed 3 years ago by monoidal

I think we can make an exception and remove the warning flag in 7.12. There's no point in explicitly specifying it, and if someone needs to use -fno-warn-context-quantification, his code will break in 7.12 anyway.

Richard: When I was implementing this almost a year ago, I downloaded the entire hackage archive and did

grep -r "type.*=.* =>" --include=*s | grep -v "forall"

and manually filtered out correct uses. This found 46 errors in 26 packages. This number is an underestimation, since it does not count "data", multiline definitions or other situations affected by the change (TH type quotations or signatures such as forall b. b -> (Ord a => a)). Based on this, I decided to make it a warning first. I can investigate further if needed.

Simon: We cannot use Explicit instead of Qualified because Explicit has precedence over Implicit, and valid code such as f :: Ord a => a -> b -> a; f = const would break.

comment:21 Changed 3 years ago by liyang

Cc: ghc.haskell.org@… added

comment:22 Changed 2 years ago by kanetw

Is anyone working on the changes Simon mentioned? Otherwise I'll go ahead and implement them.

comment:23 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:24 Changed 2 years ago by simonpj

Owner: set to simonpj

Yes, I am working on it, as part of some refactoring in the front end that I'm busy with. Thanks for the offer though! (There are plenty of other tickets, so you should not lack for opportunity.)

Simon

comment:25 Changed 2 years ago by simonpj

I think this ticket is now done (as part of the "wildcard refactor" patch (1e041b7382b6aa329e4ad9625439f811e0f27232), except that we should remove -fwarn-context-quantification altogether (according to comment:20), or deprecate it. It already does nothing.

Ben: could you do this, and close?

Simon

comment:26 Changed 2 years ago by simonpj

Owner: changed from simonpj to bgamari

comment:27 Changed 2 years ago by bgamari

Differential Rev(s): Phab:D211Phab:D211, Phab:D1615
Status: newpatch

comment:28 Changed 2 years ago by Ben Gamari <ben@…>

In ddde542d/ghc:

DynFlags Remove -fwarn-context-quantification flag

As mentioned in #4426 these warnings are now errors since the Great
Wildcards Refactor of 2015 (1e041b7382b6aa329e4ad9625439f811e0f27232).
I've opened #11221 to ensure we remove the last traces of the option in
8.2.

Test Plan: validate

Reviewers: austin

Subscribers: thomie

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

GHC Trac Issues: #4426

comment:29 Changed 2 years ago by bgamari

Resolution: fixed
Status: patchclosed

I've opened #11221 to ensure that the last traces of this flag are removed next release.

comment:30 Changed 2 years ago by Lemming

I defined a type like this one:

newtype T a = Cons (Eq a => b)

and GHC-7.10 gave me the warning:

    Variable ‘b’ is implicitly quantified due to a context
    Use explicit forall syntax instead.
    This will become an error in GHC 7.12.
    In the type ‘Eq a => b’
    In the definition of data constructor ‘Cons’

In this case my mistake was to forget to add the 'b' as type parameter, thus the advice "Use explicit forall syntax instead" was misleading. Could you write instead "Use explicit forall syntax instead or add a type parameter"?

comment:31 Changed 2 years ago by simonpj

Ah well, GHC 8.0 implements the simpler quantification rules, and now just says

T4426.hs:5:29: error: Not in scope: type variable `b'

which at least isn't misleading!

Note: See TracTickets for help on using tickets.