More explicit foralls (GHC Proposal 0007)

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



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


Diff Detail

rGHC Glasgow Haskell Compiler
Automatic diff as part of commit; lint not applicable.
Automatic diff as part of commit; unit tests not applicable.
There are a very large number of changes, so older changes are hidden. Show Older Changes
goldfire added inline comments.Jul 3 2018, 11:56 AM

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.


Indeed, yes it does.


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


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.


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


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


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


This will get removed with the refactor mentioned above.


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




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.


You may as well let-bind mkRuleTyVarBndrs $2.


Don't match and ignore feqn_bndrs.


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.






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


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

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



Then don't match on it.


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.

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.


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


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.


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


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


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


Proxy and Bool aren't type variables.


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


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




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.


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


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


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.


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.


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.)


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


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".


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...


Also added an assertion here.


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
    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

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.


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


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


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


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


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.

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.


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.


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/ to indicate what parts of the Template Haskell API you've changed? The next version of the template-haskell library will likely be, so I would go ahead and add a new version summary at the top. Something like:

## *TBA*

* <summary of your changes here>


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.


Yes, this looks good to me now.


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, where you can merge my work into your own.

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


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:

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

mayac marked 17 inline comments as done.Oct 4 2018, 3:50 PM
mayac updated this revision to Diff 18217.Oct 4 2018, 3:58 PM

Pre final rebase: addresses all outstanding comments.

mayac added inline comments.Oct 4 2018, 4:11 PM

This is the only remaining comment. @alanz is this okay?


It's worth noting that right now I have it so that warnings on unused forall'd tyvars are turned on by the -Wunused-foralls flag (which is implied by -Wall), while such warnings when no explicit forall is present, as before, are only turned on by the -Wunused-type-patterns flag (which is *not* implied by -Wall). Is this sensible?

RyanGlScott added inline comments.Oct 5 2018, 8:01 AM

I'm not @alanz, but I feel qualified enough to answer this question: what you have here is fine. There was a time where these sorts of comments attempted to state in precise detail which API annotations could emerge from certain AST forms. But ultimately, attempting to enforce this by way of comments in the GHC source code proved to be too difficult of a task. (Nowadays, the canonical reference for where API annotations can live is the ghc-exactprint project, I believe, which has more robust checking for this sort of thing.)

I'm not sure what's to become of the remaining API annotation comments in the GHC source code in the future, but what you have here is fine, since these comments aren't enforced in the first place.


Hrm, this is a really good point that I hadn't considered before. Both -Wunused-foralls and -Wunused-type-patterns make the assumption that they're warning about unused binding forms. But when you have something like:

forall a.   F a     = ()

It's unclear to me which of the two occurrences of a counts as the binding form.

If the forall a. part is the binding form, then it feels downright silly to me to claim that the a in F a is unused (by way of -Wunused-type-patterns), because it feels like F a should count as a "use" of a (i.e., F a isn't binding a at all). I suppose a similar situation arises in RULES when you have something like:

{-# RULES "f rule" forall a. f a = () #-}

f :: a -> ()
f a = ()
{-# NOINLINE [1] f #-}

In f rule, does GHC emit a warning about a being unused?

alanz added inline comments.Oct 5 2018, 8:43 AM

@mayac, @RyanGlScott I agree that these API Annotations comments should probably be stripped out, anything in that level of detail that is not machine-checked is going to end up drifting, regardless of how much effort is put in.

If the tests show the annotations are all anchored, it should be ok.

Worst case I will pick up something when doing my (now twice yearly) ghc-exacptrint sweep over things.

The mid-term goal is to move ghc-exactprint functionality in-tree so we can include tests for it with every commit.

goldfire added inline comments.Oct 5 2018, 9:28 AM

I would say that forall a. F a = () should not produce a warning. After all, the a does have an occurrence site. I'm agnostic on the -Wall situation.

mayac marked 4 inline comments as done.Oct 9 2018, 10:51 AM
mayac added inline comments.

Ah, so it seems to me we're learning towards what I had originally, which was to only warn about unused binders when there's no explicit forall present. Though I definitely agree with Ryan that -Wunused-foralls isn't right, I still feel like forall a. F a = () deserves a warning -- since it can just as well be replaced by F _ = () in the same way as F a = (). Perhaps then -Wunused-type-patterns should ignore the forall and just look for unused pattern variables? Either way, this seems like a discussion for a different patch, so I will revert this change and proceed.

@RyanGlScott That's an interesting example! No, GHC does not emit a warning, but I would say in that case it's only because the following is not valid RULES syntax:

{-# RULES "f rule" f _ = () #-}

Just checking in here -- @mayac, you're planning on updating the behavior around warnings and then we'll be good to go?

mayac updated this revision to Diff 18479.Oct 26 2018, 10:19 PM

Final rebase and squashed commits. Ready to merge?

Haddock bump can be found at:


As per personal communication with @goldfire, this has been resolved in the way I suggested above: -Wunused-type-patterns always warns about type/kind variables unused on the right hand side of an type family equation (whether they're explicitly quantified or not) and -Wunused-foralls ignores foralls in type family instance equations all together.

goldfire added inline comments.Oct 26 2018, 11:10 PM

This code is suspicious. The Nothing case seems to be making a Maybe [TyVarBndrQ]. But the Just case seems to be making a Maybe TyVarBndrQ. They can't both be right, and the Nothing case looks right to me.

Has this been tested?

You might be able to fix this by using coreJust' and mkListTy somehow.

mayac updated this revision to Diff 18485.Oct 27 2018, 10:41 AM

Template Haskell quick fix and tests

mayac added inline comments.Oct 27 2018, 10:43 AM

Well this is what I get for trying to write Haskell code past 10 PM! This should be resolved now.

Furthermore, I've now added some tests (tests/TH_reifyExplicitForAllFams.hs and tests/TH_ExplicitForAllRules.hs) that cover the changes I've made to Template Haskell. (How did I not think to do this before?)

This revision was not accepted when it landed; it landed in state Needs Review.Oct 27 2018, 1:57 PM
This revision was automatically updated to reflect the committed changes.
int-index added a subscriber: int-index.EditedOct 27 2018, 5:00 PM

Can we also add a test case (maybe extend T15264) that the new forall forms trigger the implicit kind variables warning?

I'm talking about this warning: