[GHC] #12025: Order of constraints forced (in pattern synonyms, type classes in comments)
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple TypeApplications PatternSynonyms | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: 11513, 10928 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Ever since `TypeApplications` the order of quantification matters. It seems there are some places where the user has no control over the order: {{{#!hs 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 a type annotation `X' @[t] @t :: A [t]`, see ticket #11385 to allow `X' @[_t] @_t`, for this ticket the equality is inherent in `X` so it's no big deal). 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: {{{#!hs X' @_ @ActualType }}} or to write `[ActualType]` explicitly {{{#!hs 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) {{{#!hs pattern X'' :: forall xxx. A [xxx] pattern X'' = X }}} cannot match against a type `A a` {{{#!hs -- Works foo :: A a -> ... foo X' = ... -- Doesn't bar :: A a -> ... bar X'' = ... }}} Thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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 changed by Iceland_jack: @@ -18,3 +18,3 @@ - this without a type annotation `X' @[t] @t :: A [t]`, see ticket #11385 to - allow `X' @[_t] @_t`, for this ticket the equality is inherent in `X` so - it's no big deal). + 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). New description: Ever since `TypeApplications` the order of quantification matters. It seems there are some places where the user has no control over the order: {{{#!hs 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: {{{#!hs X' @_ @ActualType }}} or to write `[ActualType]` explicitly {{{#!hs 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) {{{#!hs pattern X'' :: forall xxx. A [xxx] pattern X'' = X }}} cannot match against a type `A a` {{{#!hs -- Works foo :: A a -> ... foo X' = ... -- Doesn't bar :: A a -> ... bar X'' = ... }}} Thoughts? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (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) {{{#!hs 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 {{{#!hs q :: forall a p. P p => p a -> Int q = q_ }}} 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (by goldfire): This ordering problem is very apparent in GADT definitions. If you say {{{#!hs 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 [https://downloads.haskell.org/~ghc/8.0.1-rc4/docs/html/users_guide/glasgow_e... #visible-type-application 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Thanks for your responses. Replying to [comment:5 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 {{{#!hs 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (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 [comment:4 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 accident I saw the ticket #6081 which quantifies in the instance signature: {{{#!hs 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: {{{#!hs -- 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 {{{#!hs 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 {{{#!hs 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' [http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html #using-notation ‘using’ notation]. In broken Idris: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Semirelated: #7100 ticket allowing variables in `class` declaration that don't appear as class parameters, this would be handy -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (by goldfire): I think the pattern synonym problem is covered by [https://github.com/ghc- proposals/ghc-proposals/pull/42 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12025: Order of constraints forced (in pattern synonyms, type classes in comments) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: duplicate | TypeApplications PatternSynonyms 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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * status: new => closed * resolution: => duplicate Comment: Yes good -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12025#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC