Clarify the scoping of existentials for pattern synonym signatures
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 Q
.
This kind of problem is related to #12108 (closed), #12179