Opened 14 months ago

Last modified 14 months ago

#12187 new bug

Clarify the scoping of existentials for pattern synonym signatures

Reported by: mpickering Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: PatternSynonyms Cc: simonpj, goldfire, Iceland_jack, mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #12108 Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

What are scoping rules for type variables in pattern synonym signatures?

We said that existentials variables are scoped as follows:

  1. Existentials scope over only the provided constraints and the

arguments, not over the result type.

type Disguised a b = b -> RP a                                                 
pattern Q :: () => Eq b => Disguised a b

However, Simon argues that Q should be accepted as if we expand the type synonym then the existentially quantified b is no longer in the result type.

Richard disagrees, he considers the result type to be Disguised a b and so b is in the result type and not in-scope. Therefore he wishes to reject this example.

The purpose of this ticket is to decide the fate of Q.

This kind of problem is related to #12108, #12179

Change History (9)

comment:1 Changed 14 months ago by mpickering

Cc: simonpj goldfire added

comment:2 Changed 14 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 14 months ago by simonpj

I propose the following:

  • The universal type variables are the ones free in
    • any explicitly-forall'd universal variables
    • the required context (if any)
    • the result type, after deleting any explicitly-forall'd existentials.
  • The existentials are all the rest
  • For this purpose the "result type" is very narrowly interpreted, as follows: first drop the required and provided contexts, if present. Now drop arrows (only). What's left is the result type. In this suggestion, even parentheses stop the "dropping arrows" bit. For example:
    pattern X :: a -> (b -> T a)
    
    Here the "result type" is (b -> T a).
  • It is an error to have an existential in the return type. This can arise using explicit quantification:
    pattern Bad :: () => forall a. T a   -- Not allowed
    

This rule is simple and predictable. For Q in the description, both a and b are universal, because the result type is Disguised a b and both a and b are free.

Moreover, you can always override it by using explicit foralls, to get what you want. E.g.

pattern Q :: () => forall b. Eq b => Disguised a b

The forall means that b is no longer free in the result type

Yes we could "look through" parens. Yes, we could "look through" type synonyms, although that is harder because scopging is determined in the renamer. But it's a slippery slope; e.g. what about type functions? I say keep it simple.

Last edited 14 months ago by simonpj (previous) (diff)

comment:4 Changed 14 months ago by simonpj

Cc: mpickering added

Is every one happy with this? Richard? Matthew? Gergo?

If so I'll go ahead.

Simon

comment:5 Changed 14 months ago by simonpj

Description: modified (diff)

comment:6 Changed 14 months ago by goldfire

And how do we reject

pattern Bad :: () => forall a. T a

Do we follow your proposed rules and then check to make sure that there are no existentials in the (expanded) return type?

comment:7 Changed 14 months ago by simonpj

There should be no existentials in the return type. So that type signature would be rejected with that message.

I'll edit comment:3 to clarify that

Simon

comment:8 Changed 14 months ago by goldfire

To clarify:

  1. In pattern Q :: () => Eq b => Disguised a b, b will be inferred to be universal, and the return type will be b -> RP a. This is slightly different than the original Disguised example from the paper, in that the original example suggested that the return type be RP a.
  1. In pattern R :: (a -> Maybe a), R is a nullary pattern synonym, because the "find return type" algorithm doesn't look through parentheses. pattern R a = Just a would be rejected. R's type is distinct from pattern R2 :: a -> Maybe a, which is a unary pattern synonym.

Perhaps when describing this feature, we should be clear that the syntax of a pattern signature is this:

  • It has a nested structure. The top-level is a triple of things (the universals, the existentials, and the term-level typing information), separated by =>.
  • If no => are present, then the one item is really the term-level typing information.
  • If one => is present, then the first item is the universals, and the second item is the term-level typing information.
  • Both the universals and existentials have the same syntax: an optional forall ..., followed by a constraint.
  • The term-level typing information is a list of types, with at least one element. The list separator is spelled ->.
  • The last type in the list is the return type. All other types (there may be none) are argument types.

I've (briefly) tried to write out the BNF-style grammar here, but that's surprisingly challenging. For example, forall a. blah makes is accepted, but what does forall a. forall b. blah mean? Is b existential? Or do we need a () => to make that happen?

This is all horribly complicated!

comment:9 Changed 14 months ago by simonpj

I don't think it's complicated.

qualifier ::= forall tv1 .. tvn.
           |  forall tv1 .. tvn. ctxt =>
           | ctxt =>

body ::= btype -> body
      |  type   -- without an arrow at the top

pat_ty ::= qualifier qualifier body   -- Univ and ext
         | qualifier body             -- Univ only 
         | body

A qualifier has a forall or => or both. A pattern type has zero, one, or two qualifiers.

Needless to say I'm open to better ideas. But we need SOME way to specify it.

Note: See TracTickets for help on using tickets.