Opened 2 years ago

Closed 9 months ago

## #12025 closed feature request (duplicate)

# Order of constraints forced (in pattern synonyms, type classes in comments)

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler (Type checker) | Version: | 8.1 |

Keywords: | TypeApplications PatternSynonyms | Cc: | mpickering |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | 11513, 10928 | Differential Rev(s): | |

Wiki Page: |

### Description (last modified by )

Ever since `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 `[ActualType]`

explicitly

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 `A a`

-- Works foo :: A a -> ... foo X' = ... -- Doesn't bar :: A a -> ... bar X'' = ...

Thoughts?

### Change History (10)

### comment:1 Changed 2 years ago by

Description: | modified (diff) |
---|

### comment:3 Changed 2 years ago by

My gut tells me that this is less of an issue for type classes since quite often you want to supply the named/instance type first.

Still I need this every once in a while

### comment:4 follow-up: 7 Changed 2 years ago by

This ordering problem is very apparent in GADT definitions. If you say

data X b where MkX :: forall a b. a -> b -> X b

you get `MkX :: forall b a. a -> b -> X b`

. See the last bullet in the manual.

It would be straightforward, syntactically, to fix this for GADTs. The implementation is a bit more involved, because GHC assumes that universals come before existentials. This is surmountable with some engineering.

We should consider this problem in concert with allowing visible type patterns (#11350), because we want patterns to be able to match existentials but not universals. It's very unclear how to do this in a way that will be sane to users.

I don't have a good idea for a new syntax for dealing with this in pattern synonyms.

As for classes, I'm not as bothered. The workaround is straightforward. Furthermore, we don't currently give full type signatures for class methods, always leaving off the class constraint. (I don't see how #11620 relates to this.)

If we are going to be bothered about classes, we should also be bothered about record seleectors. But I vote not to be bothered about anything except data constructors and pattern synonyms.

### comment:5 follow-up: 6 Changed 2 years ago by

One possibility would be to use the same rules for pattern synonyms as for GADTs. When you write a GADT

data A a where X :: A [xxx]

you mean

X :: forall t. forall xxx. (t~[xxx]) => A t

so that it matches against a value of type `A ty`

for any `ty`

.

We could do the same for pattern synonyms, so that

pattern X' :: () => forall xxx. A [xxx]

means precisely

pattern X' :: forall t. () => forall xxx. (t ~ [xxx]) => A t

Perhaps we could do without the leading `() =>`

; I'm not sure.

This doesn't deal with the whole issue (as Richard points out, GADTs themselves have a smaller problem), but it ameliorates it and makes it the same as GADTs.

### comment:6 Changed 2 years ago by

Thanks for your responses.

Replying to simonpj:

We could do the same for pattern synonyms, so that

pattern X' :: () => forall xxx. A [xxx]means precisely

pattern X' :: forall t. () => forall xxx. (t ~ [xxx]) => A t

That sounds like a step in the right direction Simon but would this make the current meaning of

pattern X' :: () => forall xxx. A [xxx]

inexpressible (a pattern that only matches `A [xxx]`

)?

I want to be aware of the trade-offs, I don't have use for it personally

### comment:7 Changed 2 years ago by

8.1.20160503

ghci> class P (p :: Type -> Type) where pee :: p a -> Int ghci> :set -fprint-explicit-foralls ghci> :t pee pee :: forall {a} {p :: Type -> Type}. P p => p a -> Int

`a`

appears before `p`

, but does not apply in that order? This is surprising behaviour to me:

ghci> instance P Maybe where pee = length ghci> :t pee @Maybe pee @Maybe :: forall {a}. Maybe a -> Int ghci> :t pee @Maybe @() pee @Maybe @() :: Maybe () -> Int

Replying to goldfire:

As for classes, I'm not as bothered. The workaround is straightforward.

I wonder if you could just mention the variable before the instance but that is disallowed in `class`

declarations. Something silly `class a ~ a => P p where pee :: p a -> Int`

.

By coincidence I saw #6081 which quantifies in the instance signature:

instance forall (a :: k). KindClass (KP :: KProxy [k])

I had no idea this was allowed, it seems to only refer to variables in the instance head, when I try to use it:

-- error: -- • Couldn't match type ‘a1’ with ‘a’ instance forall a. P Maybe where pee :: Maybe a -> Int pee = length

Currently disallowed in class declarations, but what if

class forall a. P (p :: Type -> Type) where pee :: p a -> Int

meant that `a`

appears before `p`

in methods? The downside is that this would apply to every method across the board leaving no way to write siblings with a different order

class Q q where cue_1 :: q a -> Int cue_2 :: q a -> Int -- cue_1 :: forall q a. Q q => q a -> Int -- cue_1 :: forall a q. Q q => q a -> Int

This may just be inherent in the way type classes are structured, reminds me of Idris' ‘using’ notation. In broken Idris:

using (q:Type -> Type) using (a:Type) cue_1 : q a -> Int cue_2 : q a -> Int using (a:Type) using (q:Type -> Type) cue_1 : q a -> Int cue_2 : q a -> Int

It isn't a show-stopper for type classes as Richard says, just nice to have. I hadn't even thought of record selectors.

### comment:8 Changed 2 years ago by

Semirelated: #7100 ticket allowing variables in `class`

declaration that don't appear as class parameters, this would be handy

### comment:9 Changed 9 months ago by

I think the pattern synonym problem is covered by this ghc-proposal and that the GADT problem is covered by #11721. If that's the case, this ticket is redundant. Please close if you agree.

**Note:**See TracTickets for help on using tickets.

Another place I've discovered this is in type classes (I want to hear about other cases), let's say that for what ever reason want to supply the type

`a`

first but we can't (by design)Unlike the pattern synonym case this can be remedied by new function

Users will have to define a different method than they use, it's inelegant but it works. This isn't a problem if we allow signatures with explicit quantification for type classes #11620