Clarify the scoping of existentials for pattern synonym signatures
|Reported by:||mpickering||Owned by:|
|Keywords:||PatternSynonyms||Cc:||simonpj, goldfire, Iceland_jack, mpickering|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||#12108||Differential Rev(s):|
Description (last modified by )
What are scoping rules for type variables in pattern synonym signatures?
We said that existentials variables are scoped as follows:
- 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