Weird scoping for tyvars in rules

[rl]

This rule:

{-# RULES "id" forall (x :: a). id x = x #-}

compiles fine with no LANGUAGE options but fails if I add Rank2Types:

Not in scope: type variable `a'

It compiles fine again if I additionally include ScopedTypeVariables. This looks wrong to me.

[rl]

Forgot to mention: this is perhaps related to #2494.

[simonpj]

Ah, there are a bunch of issues here. Two other closely related tickets are #2498 and #2213. I'll write some notes here to cover all three. I have not executed any of the actions; I'm interested to know what others think

• RULES pragmas can't be parsed if the lexer isn't recognising 'forall' as a keyword (you'd get parse errors immediately). So the lexer only recognises RULES as a pragma if the lexer's explicitForallBit is on. Currently that bit is switched on by the extensions ScopedTypeVariables, PolymorphicComponents, ExistentialQuantification, Rank2Types, and RankNTypes.

• If one of these flags isn't on, the lexer pretends not to recongise the RULES pragma, which in turn gives an "unrecognised pragma" error in the HEAD. That seems wrong, regardless of flags: it's a perfectly good pragma.

• ACTION 1: We should have a language extension -XRewriteRules that makes the lexer recognise RULES pragmas. If -XRewriteRules is not on, they should be silently ignored as comments.

• ACTION 2: The -XRewriteRules extension should enable 'forall' as a keyword (the explicitForAllBit).

• In a RULE, the 'forall' binds only *term*-variables. You can't say RULES "foo" forall a (x::a). <blah>. There's no reason in principle why not, but we'd need syntax to distinguish term from type variables, so I don't propose to change this.

• So type variables are brought into scope much as they are in a pattern match, such as (\(x::a) -> blah). At the moment, you have to specify *both* -XPatternSignatures to allow such a type signature in a pattern at all; and -XScopedTypeVariables to allow the type variable to have scope This is a bit confusing, but it does make sense to have -XPatternSignatures without -XScopedTypeVariables; you migh say (\(x::Int)-> blah) for example.

ACTION 3: still, I propose that -XScopedTypeVariables *implies* -XPatternSignatures.

• Currently if you use -XPatternSignatures without -XScopedTypeVariables for (\(x::a) -> blah) you get

           T2497.hs:3:28: Not in scope: type variable `a'
  

And you can see why now!

• RULES always allow signatures on the forall'd binders; you don't need -XPatternSignatures (and I think it'd be pedantic to require it). So now you can see why you get the scope error. Possible alternatives to the status quo
  • -XRewriteRules implies -XScopedTypeVariables, in the entire module
  • We unconditionally but locally enable -XScopedTypeVariables in a rewrite rule. In some ways this would be consistent with the way that RULES allow signatures without a flag

ACTION 4: Opinions?

• The flag -frewrite-rules is actually an *optimisation* flag. If it's off, the Simplifier doesn't apply any rules at all. It's implied by -O.

ACTION 5: it looka s bit too much like a language flag. I wonder about renaming it to -fenable-rewrite-rules or -fuse-rewrite-rules

Simon

[rl]

My two pebbles...

• ACTION 1: Agreed in principle, but what about backwards compatibility? There is a lot of code with RULES and none of it uses -XRewriteRules. IMO, it would be better to always recognise RULES. Note also that RULES don't necessarily require forall; see http://www.haskell.org/ghc/docs/latest/html/users_guide/rewrite-rules.html#rule-spec for examples.

• ACTION 2: I think forall in RULES should always be recognised as a keyword. It is quite different from the other uses of forall, anyway, since it quantifies over terms, not types. Also, coupling explicitForallBit with a not obviously related language feature seems wrong. If forall isn't always recognised in RULES, we should have a separate -XForallKeyword (perhaps we should have that anyway).

• ACTION 3: I think the two should be kept separate but don't really care either way.

• ACTION 4: Enable -XScopedTypeVariables locally. Does -XPatternSignatures apply to RULES somehow? If so, enable this locally as well.

• ACTION 5: -fuse-rewrite-rules or -fapply... looks good to me.

• I think forall in RULES should bind type variables as well. I'm not sure new syntax is needed here: if it is used as a type, it's a type variable, otherwise it's a term variable. Or can this lead to ambiguities?

[simonpj]

After talking to Simon, and Ian, and taking on board Roman's comments, I now propose:

• Do not add -XRewriteRules. A RULE is in a pragma, and so is silently ignored by other compilers anyway. Other pragmas like SPECIALISE do not have a language extension flag. They will generate errors if they are plain wrong (e.g. variables out of scope). But adding a language flag would be inconsistent.

• Inside a RULE, switch on the forall-as-keyword in the lexer, unconditionally. Simon M will do this, and send a patch to Simon PJ for validation.

• Merge the -XScopedTypeVariables and -XPatternSignatures flags. Distinguishing them isn't senseless, but it's jolly confusing.

• Inside a RULE, switch on -XScopedTypeVariables unconditionally.

• Change -frewrite-rules to -fuse-rewrite-rules; deprecate the former.

Any dissenters?

Simon

[josef]

On the whole I think your new set of proposed changes will make things much more intuitive, especially bullets two and four. I'm stumped by the status quo every time I try to use rewrite rules.

As for bullet five, I'd prefer -fenable-rewrite-rules, simply because it has a more natural reverse: -fdisable-rewrite-rules. -fdon't-use-rewrite-rules doesn't feel quite right.

[simonpj]

Fixed by a combination of

Wed Aug 20 14:29:11 BST 2008  Simon Marlow <marlowsd@gmail.com>
  * always treat 'forall' and '.' as reserved keywords inside RULES pragmas

and

Tue Aug 26 13:21:21 BST 2008  simonpj@microsoft.com
  * Fix flaggery for RULES (cf Trac #2497)

Simon

[duncan]

Replying to simonpj:

It's not entirely obvious to me that this is all fixed, in particular this point:

* Inside a RULE, switch on -XScopedTypeVariables unconditionally.

I'm using ghc-6.10.0.20080927 and updating bytestring to use LANGUAGE pragmas rather than -fglasgow-exts. Without adding ScopedTypeVariables I get errors for the RULES pragmas:

Data/ByteString.hs:453:30: Not in scope: `forall'

Data/ByteString.hs:453:37: Not in scope: `p'

This is complaining about the code:

{-# RULES
"ByteString unpack-list" [1]  forall p  .
    unpackFoldr p (:) [] = unpackList p
 #-}

It's not clear to me what the "Right Thing" I'm supposed to do. Should I be using the ScopedTypeVariables to get RULES pragmas to be recognised? Do I need to use -fuse-rewrite-rules to have the rules actually used? What should I be using for older ghc?

[simonpj]

Finally fixed by

Wed Oct 15 09:43:44 BST 2008  simonpj@microsoft.com
  * Fix Trac #2497; two separate typos in Lexer.x

Please merge to 6.10

Simon

[igloo]

Merged