Order of constraints forced (in pattern synonyms, type classes in comments)
|Reported by:||Iceland_jack||Owned by:|
|Component:||Compiler (Type checker)||Version:||8.1|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||11513, 10928||Differential Rev(s):|
Description (last modified by )
TypeApplications the order of quantification matters.
It seems there are some places where the user has no control over the order:
data A a where X :: A [xxx] pattern X' :: forall t. () => forall xxx. t ~ [xxx] => A t pattern X' = X
This quantifies the universal
t and the existential
xxx.. but in this case
t is constrained to equal
[xxx] so when we supply our first type (the universal
t) it is forced to be of the form
[a]. Then the existential is forced to equal
a (there is currently no way to express this without quantification + annotation
X' @[t] @t :: forall t. A [t], see ticket #11385 to allow
X' @[_t] @_t, for this ticket the equality is inherent in
X so it doesn't matter).
This means that the first argument really doesn't give any further information but it seems impossible to reorder the existential type before the universal. This either forces the user to supply a dummy type:
X' @_ @ActualType
or to write
X' @[ActualType] X' @[ActualType] @ActualType X' @[_] @ActualType
This may be a bigger inconvenience than it may seem: the return type can be more complicated
A (B (C a)) and it requires the user to look it up.
X' @_ @ActualType feels like bad library design, especially as the number of existential variables grows and the user has to remember how many underscores to provide.
See also ticket:10928#comment:5
Keep in mind that this usage will be common, since the more obvious (see ticket:10928#comment:16)
pattern X'' :: forall xxx. A [xxx] pattern X'' = X
cannot match against a type
-- Works foo :: A a -> ... foo X' = ... -- Doesn't bar :: A a -> ... bar X'' = ...