Opened 10 months ago

Last modified 10 months ago

#12025 new feature request

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 Iceland_jack)

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 (8)

comment:1 Changed 10 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 10 months ago by Iceland_jack

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)

class P p where
  q_ :: forall a. p a -> Int

instance P Maybe where
  q_ :: forall a. Maybe a -> Int
  q_ = length 

Unlike the pattern synonym case this can be remedied by new function

q :: forall a p. P p => p a -> Int
q = q_ @p @a

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

Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:3 Changed 10 months ago by Iceland_jack

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 Changed 10 months ago by goldfire

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 Changed 10 months ago by simonpj

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 in reply to:  5 Changed 10 months ago by Iceland_jack

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 in reply to:  4 Changed 10 months ago by Iceland_jack

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.

Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:8 Changed 10 months ago by Iceland_jack

Semirelated: #7100 ticket allowing variables in class declaration that don't appear as class parameters, this would be handy

Note: See TracTickets for help on using tickets.