More explicit foralls (GHC Proposal 0007)
Needs ReviewPublic

Authored by mayac on Jun 25 2018, 9:33 AM.

Details

Reviewers
goldfire
bgamari
alanz
Trac Issues
#2600
#14268
Summary

Allow the user to explicitly bind type/kind variables in type and data
family instances (including associated instances), closed type family
equations, and RULES pragmas. Follows the specification of GHC
Proposal 0007, also fixes Trac #2600. Advised by Richard Eisenberg.

This modifies the Template Haskell AST -- old code may break!

Other Changes:

  • convert HsRule to a record
  • make rnHsSigWcType more general
  • add repMaybe to DsMeta
Test Plan

validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Branch
wip/yac
Lint
Lint WarningsExcuse: Roughly 80 characters
SeverityLocationCodeMessage
Warningcompiler/deSugar/DsMeta.hs:2234TXT3Line Too Long
Warningcompiler/hsSyn/HsDecls.hs:1554TXT3Line Too Long
Warningcompiler/hsSyn/HsDecls.hs:2143TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:257TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:262TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:850TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:856TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:857TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:866TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:710TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:712TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:713TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:715TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:720TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:762TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:765TXT3Line Too Long
Warningcompiler/rename/RnTypes.hs:102TXT3Line Too Long
Warningcompiler/rename/RnTypes.hs:103TXT3Line Too Long
Warningcompiler/rename/RnTypes.hs:104TXT3Line Too Long
Warningcompiler/typecheck/TcInstDcls.hs:761TXT3Line Too Long
Warningcompiler/typecheck/TcRules.hs:88TXT3Line Too Long
Warningcompiler/typecheck/TcRules.hs:155TXT3Line Too Long
Warningcompiler/typecheck/TcRules.hs:165TXT3Line Too Long
Warningcompiler/typecheck/TcSplice.hs:1718TXT3Line Too Long
Warningcompiler/typecheck/TcSplice.hs:1719TXT3Line Too Long
Unit
No Unit Test Coverage
Build Status
Buildable 22276
Build 51652: [GHC] Linux/amd64: Continuous Integration
Build 51651: [GHC] OSX/amd64: Continuous Integration
Build 51650: [GHC] Windows/amd64: Continuous Integration
Build 51649: arc lint + arc unit
mayac created this revision.Jun 25 2018, 9:33 AM
alanz added inline comments.Jun 29 2018, 4:11 AM
compiler/hsSyn/HsDecls.hs
1549

I imagine this note will need some updating.

2086

This should just be Maybe [LHsTyVarBndr pass].

Lots of little points, but very nice overall.

Note to others: I've worked with @mayac on this patch, and I know he will be on an extended holiday for some time this summer. If anyone is itching to get this in, I could push it through, but I favor leaving these loose ends for him to clean up when he returns. I'm writing this note mainly so that so one worries about a lag here. If this patch isn't addressed by October 2018, then it's time for me to commandeer.

compiler/deSugar/DsMeta.hs
348–352

This is really quite awkward. In the Just case, the second parameter (Core [TH.TyVarBndrQ]) is unused. I think some refactoring around all this is in order.

462–463

Then ASSERT this, just to be sure.

467–469

This seems wrong. Indeed, I'm not sure how this type-checks at all: it looks like we need return :: a -> DsM (Core a). I suppose there is enough freedom of metavariables here to make this work out, but using repMaybeList on Nothing seems awfully round-about. Just use coreNothing.

562–565

This also looks like it won't work: the mb_bndrs are never brought into scope. Perhaps they should be added to the hsq_explicit field above.

583–589

Here, too, the mb_bndrs are never brought into scope.

656

This would be cleaner, I think, to use addHsTyVarBinds.

compiler/hsSyn/HsDecls.hs
1549

Indeed, yes it does.

1651

No need to match and discard -- just remove this line.

2086

That doesn't quite work, sadly. The problem is that the types won't match up when we want to build RuleDecl GhcTc, as there is no LHsTyVarBndr GhcTc. I don't agree with @mayac 's use of X here for this, but the easy answer won't do.

On some thought, the pattern we see here (respecting GhcPs and GhcRn, but then changing GhcTc to GhcRn) is common enough that it should be made into a type family. This family could then be used to store, e.g., the type signature currently in XExprWithTySig.

2087

These store tyvars after type checking. Restore comment to that effect.

2096

@alanz: How should annotations work here? There are potentially now two foralls and two .s.

2164

This isn't quite right. We still need to print the forall . if there are no terms but there are types.

compiler/hsSyn/HsExtension.hs
428

This will get removed with the refactor mentioned above.

compiler/hsSyn/HsTypes.hs
1370

This is a change in behavior -- I don't think the change is wanted.

compiler/parser/Parser.y
346–368

s/conflicts/conflict/

364

NB: This is documented in the manual ("Inside a RULE “forall” is treated as a keyword, regardless of any other flag settings.") and is similar to the conflict in 753.

1677

You may as well let-bind mkRuleTyVarBndrs $2.

compiler/parser/RdrHsSyn.hs
177–178

Don't match and ignore feqn_bndrs.

862

This doesn't seem sufficient. For example, it looks like you might be able to create a tyvar spelled ++ or something -- where, in types, ++ is really like a tycon, not a tyvar. The functions in Lexeme.hs can help sort this out.

compiler/rename/RnSource.hs
712

s/freed/free/

714

s/freed/free/

733

GHC convention uses a $, not a ( before the \.

755

Why only when there's no forall? Should we warn on

type instance forall a. F (a :: k) = a

?

810

Then don't match on it.

1035–1036

Since the payload of the Maybe is unused, change to Maybe ty_bndrs. It makes it obvious that the Maybe is just a proxy for Bool then.

compiler/typecheck/TcRules.hs
85–88
Note [TcLevel in type checking rules]
~~~~~~~~~~~~~~~~~~~~~~~~
Bringing type variables into scope naturally bumps the TcLevel. Thus, we type check the term-level
binders in a bumped level, and we must accordingly bump the level whenever these binders are
in scope.

This should be referred to here and near the types for the tcRuleBndrs functions.

155

Though the problem isn't new, this is a bit wrong, as it loses type signatures.

163

This call to tcExplicitTKBndrs is the only part that bumps the level. We can call getTcLevel here, and that way tcRuleTmBndrs doesn't need to bother with it.

184

We should note here that the renamer reports errors if out-of-scope type variables are used.

compiler/typecheck/TcSplice.hs
1711

This idiom has been repeated three times. It's worth a function.

compiler/typecheck/TcTyClsDecls.hs
1292

This is always Nothing, no? Don't match on it then.

docs/users_guide/glasgow_exts.rst
7514

Proxy and Bool aren't type variables.

7725–7732

An example showing where the forall could appear would be welcome.

8036

It's worth an example, as type forall ... looks weird and we need to show that it's right.

libraries/template-haskell/Language/Haskell/TH/Lib.hs
211

No.

libraries/template-haskell/Language/Haskell/TH/Ppr.hs
546

If the type-level forall is non-empty, then we still need to print forall..

mayac marked 27 inline comments as done.Aug 14 2018, 1:14 PM

Returning to work on this, the new diff will be added shortly.

compiler/deSugar/DsMeta.hs
348–352

Hurray! I wanted to change this before but didn't feel like I had the authority mess with anything.

467–469

Huh, for some reason I remember having a problem with just coreNothing here before, but it certainly seems to work now!

562–565

I was and continue to be confused by this part of DsMeta, so I have nothing to add – though this change does makes sense. Thus even though I did what you suggested here and below, not marking as "Done" since you didn't seem 100% sure this is all that needs to happen and I have little confidence in my ability here to check that.

compiler/hsSyn/HsDecls.hs
2086

Hmm, unfortunately I don't think I know enough about GHC's constraint solver to address this. The problem revolves around the one outlined in the [OutputableX] note in HsExtension.hs – let's say we add the following type family:

type family NoGhcTc p
type instance NoGhcTc GhcPs = GhcPs
type instance NoGhcTc GhcRn = GhcRn
type instance NoGhcTc GhcTc = GhcRn

Then, in order to deduce Outputable (LHsTyVarBndr (NoGhcTc p)), for example, we would need to know there exists some pass such that NoGhcTc p ~ GhcPass pass for all p. I wasn't able to work out how to add any variant of a constraint like this to OutputableX without being yelled at about impredicative polymorphism. It's also possible to just say that whenever someone uses NoGhcTc they must put the appropriate constraint in OutputableX, but this seems non-ideal.

Perhaps then something like the following is preferable:

type family NoGhcTc (t :: * -> *) p
type instance NoGhcTc t GhcPs = t GhcPs
type instance NoGhcTc t GhcRn = t GhcRn
type instance NoGhcTc t GhcTc = t GhcRn

but I still don't know the constraint magic to make this work.

compiler/parser/Parser.y
346–368

Though this is grammatically incorrect, the standard appears to be to keep the happy output, which contains an 's' regardless of how many confict(s) are present – check all the other lines, even those I did not modify! (Happy to change this, but then I should probably go and change all the others as well.)

compiler/parser/RdrHsSyn.hs
177–178

Added an assertion as per your comment above, since here feqn_bndrs should also always be Nothing.

862

I don't know about this. The inputs to this function were necessarily parsed as varids, which presumably cannot be ++, for example. The reason this function exists at all is because the quantified type vars in rules should really have been parsed as tyvarids, which differ from varids only in disallowing "forall", "family" and "role".

compiler/rename/RnSource.hs
755

Good catch! It seems just removing this check addresses your example and any other with implicitly bound kind vars. However, an even smaller (possible) example is:

type instance forall a. F a = Bool

Looking at this now, it seems to me the presence of an explicit forall shouldn't have any effect on this warning, no? If so then I'll need to change a bit more...

810

Also added an assertion here.

compiler/typecheck/TcRules.hs
155

I don't think I understand, could you elaborate on this?

mayac marked 6 inline comments as done.Aug 14 2018, 1:17 PM
mayac updated this revision to Diff 17666.Aug 14 2018, 2:13 PM

(Some) July Phabricator revisions

Forgive me for taking so long to comment on this, but I'm somewhat confused by the pervasive use of Maybe [TyVarBndr] in this patch. Is there a reason to use this over [TyVarBndr]? Indeed, the ForallC and ForallT Template Haskell constructors already adopt the convention of using [TyVarBndr] (using an empty list to represent a lack of an explicit forall).

RyanGlScott updated the Trac tickets for this revision.Aug 14 2018, 2:38 PM
mayac added a comment.Aug 14 2018, 3:09 PM

@RyanGlScott It's to differentiate between the case where there is no explicit forall (type instance F a = ...) and where there is an empty explicit forall (type instance forall. F a = ...). Type variables on the LHS are implicitly bound only in the former case, thus the latter example would be accepted only if a is already in scope.

In D4894#139146, @mayac wrote:

Type variables on the LHS are implicitly bound only in the former case, thus the latter example would be accepted only if a is already in scope.

Right, that is a good point. I suppose by this reasoning, the [TyVarBndr] field of ForallT should really be Maybe [TyVarBndr] as well, since at present there's no way to represent this analogous example using the Template Haskell AST:

foo :: forall a. Ord a => a -> a -> Bool
foo = goo
  where
    goo :: forall. Eq a => a -> a -> Bool
    goo = (==)

But oh well—one breaking change at a time :)

goldfire added inline comments.Aug 14 2018, 10:37 PM
compiler/hsSyn/HsDecls.hs
2086

Your second NoGhcTc is what I was thinking. Then you would modify OutputableX to include Outputable instances like there exist today, enumerating all ways that NoGhcTc is used. This is very unfortunate, but I think you're right that there's no better way to proceed today.

Happily, there will be a better way in the future, thanks to the new -XQuantifiedConstraints feature, which will solve this problem nicely. However, we have to wait a little while before we can start using that in GHC itself.

compiler/parser/Parser.y
346–368

Bah. Do what you think is best. I've suddenly discovered I don't really care. :)

compiler/parser/RdrHsSyn.hs
177–178

Sounds good. It was just that it's bad style to include rec_name = _ in a pattern match.

862

Ah. I was confused. See Trac #15522. No need to make changes here, then.

compiler/rename/RnSource.hs
755

I think you're right that the presence of the forall is irrelevant here.

compiler/typecheck/TcRules.hs
155

Normally, we like to preserve user-written syntax. If I write {-# RULES "id" forall (x :: a). id x = x #-} and ask GHC to print it to me, I'd expect GHC to print it including the :: a. The treatment here means that GHC forgets the :: a was there after type-checking. There's nothing you need to do now, but it's, well, a bit wrong.

mayac marked 13 inline comments as done.Aug 15 2018, 1:36 PM
mayac added inline comments.
compiler/hsSyn/HsDecls.hs
2086

Another roadblock here: recursive modules. Recall that HsTypes.hs, HsDecls.hs, etc. all import HsExtension.hs. So suppose we define:

type LHsRuleTyVarBndr pass = NoGhcTc LHsTyVarBndr pass

In order to include the necessary lines about LHsRuleTyVarBndr in OutputableX, either this definition would need to be in HsExtension.hs, which would require HsExtension.hs importing HsTypes.hs, or in the 'right' place, HsDecls.hs, but still with HsExtension.hs importing HsDecls.hs.

Having to both modify OutputableX and mess with .hs_boot files just to use this NoGhcTc type family seems like more trouble than just defining the type family directly without NoGhcTc in my opinion. Though perhaps I'm missing something obvious.

compiler/rename/RnSource.hs
755

Done, although the resulting error messages are possibly confusing:

    Defined but not used: type variable ‘t’
    |
143 |   forall t a. F (t a) = [a]
    |          ^
    Defined but not used: type variable ‘a’
    |
144 |   forall a.   F a     = ()
    |          ^

Indeed both variables picked out by GHC can be replaced by underscores and everything will be accepted, but I feel like the language "Defined by not used" might be confusing, since in a sense they are used, just not in an essential way. Do you also share this sentiment?

If Richard and Ryan are happy, then I am.

Please ask if there are any particular bits you want me to look at.

Simon

To further pass the buck, if Richard is happy with this, then so am I.

I have one minor request to make: can you update libraries/template-haskell/changelog.md to indicate what parts of the Template Haskell API you've changed? The next version of the template-haskell library will likely be 2.15.0.0, so I would go ahead and add a new version summary at the top. Something like:

## 2.15.0.0 *TBA*

* <summary of your changes here>

Thanks!

I'm on holiday at the moment and haven't taken a look at this since my last volley of comments. Will re-engage next week! Until then, don't interpret my silence as anything but the fact that I'm enjoying less screen time. :)

This one got lost in the shuffle a bit -- apologies.

See below. And please don't forget about Ryan's request about TH changes.

compiler/deSugar/DsMeta.hs
562–565

Yes, this looks good to me now.

compiler/hsSyn/HsDecls.hs
2086

I refused to take no for an answer here and tried it myself. It was harder going than I thought, but it all came together in the end. Please see https://github.com/m-yac/ghc/pull/1, where you can merge my work into your own.

Now, you might be able to refactor this bit as I've suggested...

compiler/rename/RnSource.hs
755

Good catch. Can we rephrase the message to, say, "Defined but not used on the right-hand side"?

Which GHC proposal is this implementing? Not Trac #7, I think: https://github.com/ghc-proposals/ghc-proposals/pull/7/files

Anyway, I think it'd be good to get on with this!