[GHC] #8779: Exhaustiveness checks for pattern synonyms
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------------+------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: -------------------------------------------+------------------------------- Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting! Another missing piece is exhaustiveness checks. Given this pattern {{{ initLast [] = Nothing initLast xs = Just (init xs, last xs) pattern xs ::: x <- (initLast -> Just (xs,x)) }}} we want the compiler to tell the programmer that {{{ f [] = ... f (xs ::: x) = ... }}} is complete, while {{{ g (xs ::: x) = ... }}} is not. With view pattern directly, this is impossible. But the programmer did not write view patterns! So here is what I think might work well, inspired by the new `MINIMAL` pragma: We add a new pragma `COMPLETE_PATTERNS` (any ideas for a shorter name). The syntax is essentially the same as for `MINIMAL`, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case. {{{ {-# COMPLETE_PATTERNS [] && (:::) #-} }}} Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors. When checking for exhaustiveness, this would be done before unfolding view patterns, and for `g` above we get a warning that `[]` is not matched. Again, the implementation is very much analogous to `MINIMAL`. Clearly, a library author can mess up and give wrong `COMPLETE_PATTERNS` pragmas. I think that is ok (like with `MINIMAL`), and generally an improvement. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms --------------------------------------------+------------------------------ Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by merijn): * cc: merijn@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms --------------------------------------------+------------------------------ Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by dfranke): * cc: dfranke (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms --------------------------------------------+------------------------------ Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by dfranke): In the common case where all pattern synonyms in a set of binding clauses are simply bidirectional, exhaustiveness can be inferred automatically. It would be nice if GHC did this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.6.3 Component: Compiler | Keywords: pattern synonyms (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by cactus): * keywords: => pattern synonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.6.3 Component: Compiler | Keywords: pattern synonyms (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by Artyom.Kazak): * cc: yom@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.6.3 Component: Compiler | Keywords: PatternSynonyms (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by cactus): * keywords: pattern synonyms => PatternSynonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.6.3 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by cactus): Just thinking out loud here, but does the PatternMatchCheck story have something to offer us here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.6.3 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by Feuerbach): * cc: roma@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by hvr): * version: 7.6.3 => 7.8.1 Comment: GHC 7.6 didn't support `PatternSynonyms` yet -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by anders_): * cc: hello@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * cc: mpickering (added) Comment: I don't think that any solution which 'looks through" pattern synonyms is desirable as it would break the abstraction. I think that Joachim's suggestion is perhaps a bit better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by hvr): I just stumbled over an annoying case due to our new `ErrorCall` in GHC 8.0: {{{#!hs {-# LANGUAGE PatternSynonyms #-} module Patterns where -- import Control.Exception (ErrorCall(..)) data ErrorCall = ErrorCallWithLocation String String deriving (Eq, Ord) pattern ErrorCall :: String -> ErrorCall pattern ErrorCall err <- ErrorCallWithLocation err _ where ErrorCall err = ErrorCallWithLocation err "" getMsg :: ErrorCall -> String getMsg (ErrorCall y) = y getMsg' :: ErrorCall -> String getMsg' (ErrorCallWithLocation y _) = y }}} With that, GHC HEAD currently warns {{{ patterns.hs:12:1: warning: Pattern match(es) are non-exhaustive In an equation for ‘getMsg’: Patterns not matched: _ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * cc: gkaracha (added) Comment: CCing George Karachalias, who is responsible for our greatly improved new exhaustiveness checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by bgamari: Old description:
Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting!
Another missing piece is exhaustiveness checks. Given this pattern {{{ initLast [] = Nothing initLast xs = Just (init xs, last xs) pattern xs ::: x <- (initLast -> Just (xs,x)) }}} we want the compiler to tell the programmer that {{{ f [] = ... f (xs ::: x) = ... }}} is complete, while {{{ g (xs ::: x) = ... }}} is not.
With view pattern directly, this is impossible. But the programmer did not write view patterns!
So here is what I think might work well, inspired by the new `MINIMAL` pragma:
We add a new pragma `COMPLETE_PATTERNS` (any ideas for a shorter name). The syntax is essentially the same as for `MINIMAL`, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case.
{{{ {-# COMPLETE_PATTERNS [] && (:::) #-} }}}
Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors.
When checking for exhaustiveness, this would be done before unfolding view patterns, and for `g` above we get a warning that `[]` is not matched. Again, the implementation is very much analogous to `MINIMAL`.
Clearly, a library author can mess up and give wrong `COMPLETE_PATTERNS` pragmas. I think that is ok (like with `MINIMAL`), and generally an improvement.
New description: Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting! Another missing piece is exhaustiveness checks. Given this pattern {{{#!hs initLast [] = Nothing initLast xs = Just (init xs, last xs) pattern xs ::: x <- (initLast -> Just (xs,x)) }}} we want the compiler to tell the programmer that {{{#!hs f [] = ... f (xs ::: x) = ... }}} is complete, while {{{#!hs g (xs ::: x) = ... }}} is not. With view pattern directly, this is impossible. But the programmer did not write view patterns! So here is what I think might work well, inspired by the new `MINIMAL` pragma: We add a new pragma `COMPLETE_PATTERNS` (any ideas for a shorter name). The syntax is essentially the same as for `MINIMAL`, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case. {{{#!hs {-# COMPLETE_PATTERNS [] && (:::) #-} }}} Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors. When checking for exhaustiveness, this would be done before unfolding view patterns, and for `g` above we get a warning that `[]` is not matched. Again, the implementation is very much analogous to `MINIMAL`. Clearly, a library author can mess up and give wrong `COMPLETE_PATTERNS` pragmas. I think that is ok (like with `MINIMAL`), and generally an improvement. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by liyang): * cc: liyang (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) Comment: I suspect making this really work right may require some modifications to the pattern synonym concept. For example, {{{#!hs pattern Empty = Seq EmptyT pattern x :<| xs <- (viewl -> x :< xs) pattern xs :|> x <- (viewr -> xs :> x) }}} To see that either `x :<| xs` or `xs :|> x` is complete when combined with `Empty`, the exhaustiveness checker would have to recognize that `viewl` and `viewr` will give non-empty results under the same circumstances. This may be feasible in this case (I'm not sure), but in principle it seems rather hard. I think a good target would be to ensure that multiple pattern synonyms using the ''same'' view are handled properly. An alternative blunt instrument: let the user promise that a certain combination of pattern synonyms will always be exhaustive when applied to a particular type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Oh, I see that was proposed initially. Duh! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by akio): * cc: akio (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by hesselink): * cc: hesselink (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mgsloan): * cc: mgsloan (added) Comment: +1 for resolving this (though I realize it's tricky)! Stack's build on 8.0 has this issue with ErrorCall's pattern synonym. Due to `-fwarn- incomplete-uni-patterns`, `catch f (\(ErrorCall x) -> g x)` causes a non- exhaustive case warning. See https://github.com/commercialhaskell/stack/pull/2145#issuecomment-219472907 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Here's a crazy idea, associate every pattern synonym with a data type (this could also be a new ‘form’ of pattern synonyms). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:22 Iceland_jack]:
Here's a crazy idea, associate every pattern synonym with a data type (this could also be a new ‘form’ of pattern synonyms).
Yes, sometimes, but when pattern synonyms overlap (e.g., left and right views, with empty), life sucks again. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:23 dfeuer]:
Yes, sometimes, but when pattern synonyms overlap (e.g., left and right views, with empty), life sucks again.
`MINIMAL` pragmas allow conjunction as well as disjunction {{{#!hs {-# MINIMAL fromRational, (recip | (/)) #-} }}} If you want to express that `Empty` and `(:<|)` form a complete pattern but so does `Empty` and `(:|>)` {{{#!hs pattern Empty :: Seq.Seq a pattern Empty <- (Seq.viewl -> Seq.EmptyL) where Empty = Seq.empty pattern (:<|) :: a -> Seq.Seq a -> Seq.Seq a pattern x :<| xs <- (Seq.viewl -> x Seq.:< xs) where x :<| xs = x Seq.<| xs pattern (:|>) :: Seq.Seq a -> a -> Seq.Seq a pattern xs :|> x <- (Seq.viewr -> xs Seq.:> x) where xs :|> x = xs Seq.|> x }}} so what's stopping us from writing {{{#!hs {-# COMPLETE_PATTERNS (Empty, (:<|)) | (Empty, (:|>)) #-} }}} to mean just that? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): The ticket mentions
Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors.
which sounds like {{{#!hs {-# COMPLETE_PATTERNS Empty, (:<|) #-} {-# COMPLETE_PATTERNS Empty, (:|>) #-} }}} would equal what I proposed (if I got the precedence right) {{{#!hs {-# COMPLETE_PATTERNS Empty, (:<|) | Empty, (:|>) #-} }}} ---- Tangent: The second part (“there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors.”) sounds awful similar to this part of the [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/pragmas.html users guide]:
If no MINIMAL pragma is given in the class declaration, it is just as if a pragma {{{#!hs {-# MINIMAL op1, op2, ..., opn #-} }}} was given, where the `opi` are the methods a. that lack a default method in the class declaration, and b. whose name that does not start with an underscore (c.f. -fwarn- missing-methods, Section 4.8, “Warnings and sanity-checking”).
As I understand it means that when the user defines {{{#!hs data ABC = A | B | C }}} it is as if the she had also written `{-# COMPLETE_PATTERNS A, B, C #-}`. Would this work with GADTs? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Keeping in mind that the patterns `Empty`, `(:<|)`, `(:|>)` may be defined in separate modules. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ekmett): * cc: ekmett (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): One use case, GHC has a type {{{#!hs data GenLocated l e = L l e }}} It's common to see code where the location information is ignored `L _ xxx` {{{#!hs -- data RuleBndr name -- = RuleBndr (Located name) -- | RuleBndrSig (Located name) (LHsSigWcType name) ... get_var (L _ (RuleBndrSig v _)) = v get_var (L _ (RuleBndr v)) = v }}} Ignoring whether it would be a worthwhile for GHC we define {{{#!hs {-# COMPLETE_PATTERNS LRuleBndr, LRuleBndrSig #-} pattern LRuleBndr a <- L _ (RuleBndr a) pattern LRuleBndrSig a b <- L _ (RuleBndrSig a b) }}} this becomes error prone for larger AST like `StmtLR`, especially when more cases get added {{{#!hs {-# COMPLETE_PATTERNS L_ #-} pattern L_ a <- L _ a {-# COMPLETE_PATTERNS LLastStmt, LBindStmt, LApplicativeStmt, (LLetStmt | LLetStmtL), -- ? ... #-} pattern LLastStmt a b c <- L_ (LastStmt a b c) pattern LBindStmt a b c d e <- L_ (BindStmt a b c d e) pattern LApplicativeStmt a b c <- L_ (ApplicativeStmt a b c) pattern LBodyStmt a b c d <- L_ (BodyStmt a b c d) pattern LLetStmt a <- L_ (LetStmt a) pattern LLetStmtL a <- L_ (LetStmt (L_ a)) ... }}} It is increasingly clear to me that ''some form'' of exhaustivity inference is needed, but that's all I've got. ---- Do we allow mixing {{{#!hs {-# COMPLETE_PATTERNS None, Just | Nothing, Some | None, Some #-} pattern None = Nothing pattern Some x = Just x }}} can this be inferred as exhaustive {{{#!hs -- data ErrorCall = ErrorCallWithLocation String String pattern ErrorCall err <- ErrorCallWithLocation err _ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms
-------------------------------------+-------------------------------------
Reporter: nomeata | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.8.1
checker) | Keywords:
Resolution: | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Iceland_jack):
=== Halfbaked thought
Map to constructors whose exhaustivity information is known.
{{{#!hs
{-# PATTERN
Empty = EmptyL
x :<| xs = x :< xs
xs :|> x = x :< xs
#-}
pattern Empty <- (Seq.viewl -> Seq.EmptyL)
pattern x :<| xs <- (Seq.viewl -> x :< xs)
pattern xs :|> x <- (Seq.viewr -> xs :> x)
}}}
{{{#!hs
{-# PATTERN
None = Nothing
Some x = Just x
#-}
pattern None = Nothing
pattern Some x = Just x
}}}
{{{#!hs
{-# PATTERN
ErrorCall err = ErrorCallWithLocation err _
#-}
pattern ErrorCall err <- ErrorCallWithLocation err _
}}}
{{{#!hs
{-# PATTERN
LLastStmt a b c <- L _ (LastStmt a b c)
LBindStmt a b c d e <- L _ (BindStmt a b c d e)
LApplicativeStmt a b c <- L _ (ApplicativeStmt a b c)
...
#-}
pattern LLastStmt a b c <- L _ (LastStmt a b c)
pattern LBindStmt a b c d e <- L _ (BindStmt a b c d e)
pattern LApplicativeStmt a b c <- L _ (ApplicativeStmt a b c)
...
}}}
Then whenever the solver encounters
{{{#!hs
len Empty = 0
len (xs :|> _) = 1 + len xs
}}}
it is as if the user had written the exhaustive `len EmptyL = ...; len
(_:
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I have to say I don't care for this `COMPLETE_PATTERNS` pragma at all, for several reasons: * In general there may be many sets of complete patterns for a data type, and ensuring that the `COMPLETE_PATTERNS` are correct and complete may be difficult. * The `COMPLETE_PATTERNS` pragmas are hand-written and unchecked, and therefore likely to go out of date as the data type changes, making pattern exhaustiveness checking unreliable. * Unlike the situation of type class methods with their `MINIMAL` pragmas, any module can define new view patterns for a given data type. How can two different modules cooperate to produce new sets of complete patterns containing pattern synonyms from both modules? * Also unlike type classes, it's not obvious (to me anyways) that there is a unique best way to use the information of the `COMPLETE_PATTERNS` pragmas, as pattern matches can be nested. Overall this proposed new feature doesn't seem to offer a very compelling solution (for full disclosure, I don't consider the problem of pattern synonym exhaustiveness checks particularly compelling in the first place; seems like scope creep). I would prefer something simple like * Pattern synonyms are checked for exhaustiveness as though they were expanded to their definitions. No hand-written pragmas needed. * GHC understands that if `p1`, ..., `pn` are exhaustive patterns for the result type of `f`, then `f -> p1`, ..., `f -> pn` are exhaustive patterns for the input type of `f`. This to some extent solves the problem of mixing patterns defined in different modules, as long as those patterns are defined in terms of the same "view functions". In some cases this may require defining several equivalent patterns with different definitions, such as `EmptyL` and `EmptyR`. This seems quite acceptable to me and probably clarifies the intent at the use site of the pattern anyways. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): What you say is attractive Reid, but consider a snoc-view of a list. We might want to say that the two patterns `SnocNil` and `SnocCons` are exhaustive, but the fact that they are really is something that needs proof (`SnocCons` at least is defined via a view). Moreover, if we match on `SnocCons` and miss out `SnocNil` we'd like to report `SnocNil` as missing, rather than `[]`. And vice versa with matching on `SnocNil` and omitting `SnocCons`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): You can define `SnocNil` via the same view (e.g. `viewr -> EmptyR`), then from my last bullet point GHC will see that the patterns are exhaustive. There will certainly be other holes in the scheme though. Even if we had `COMPLETE_PATTERNS`, I would still expect GHC to be able to handle expanding pattern synonyms to their definitions and collecting view patterns with the same view without any help from `COMPLETE_PATTERNS` pragmas; and then I don't see much additional value in the pragma to justify its implementation given its limitations. I could get behind a more comprehensive solution, though I don't know what it would look like. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Reid, your first of bullet points makes a lot of sense to me but I am still worried about abstraction. For example, the only way to construct and deconstruct `Command`s is by using `AddOne` and `MinusOne` thus a complete set of patterns would be `AddOne` and `MinusOne`. When looked through, there are many more values which inhabit this type. So it seems under your proposal that this would cause a warning. {{{ module M ( Command(AddOne, MinusOne) ) where data Command = Command String pattern AddOne = Command "AddOne" pattern MinusOne = Command "MinusOne" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): In a case like this you would define a view `data CommandView = A1 | M1; viewCommand :: Command -> CommandView` which is presumed to be total thanks to your invariant. Then define `pattern AddOne = (viewCommand -> A1)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * owner: => mpickering -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:36 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I still hope you're not planning to implement `COMPLETE_PATTERNS` :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * differential: => Phab:D2669 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:38 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Just to check: as I understand it, you are working on this, but it's not ready for review. Can I urge you to write a ''specification'' of what you are trying to achieve? A wiki page is a good place to do that. It's super-hard to review code without knowing (precisely) what it is trying to do. And it's annoying for you if people suggest changes to the spec after you have already invested a lot in the impl. Thanks for doing this! Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): The specification is on the wiki. https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs The implementation is also finished and split up into two patches. One which refactors the pattern match checker (D2725) and one which implements the feature. (D2669) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:40 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK thanks, I did not know that. So are you declaring the specification and both patches ready for review? Worth sending an email to ghc-devs about that. Also, I hate to suggest this, but it looks like an ideal candidate for a GHC proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:41 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Yes everything should be ready for review. I just posted to the mailing list about it. I'm not interested in submitting a GHC proposal until there is a process for proposals to be actually accepted. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:42 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Changes (by lelf): * cc: lelf (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:43 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Somehow I've not looked at this thread, finding this only by a mention of `COMPLETE` elsewhere. (This is my fault -- just explaining my silence on this topic which is in my area of interest.) A few nitpicks about the specification: - The wiki page uses "total" in several places, but I think you mean "covering". I use "total" to refer to functions that are both covering and terminating. - Would the following be acceptable? {{{ data Void data T = T1 Int | T2 Bool | T3 Void {-# COMPLETE T1, T2 #-} }}} It would seem so. I'm happy for this to be accepted; I'm just stress- testing the spec. - The argument for not having the pattern-match checker look through pattern synonyms is reasonable. But is there a way to have GHC do some checking on `COMPLETE` declarations? It would be great -- especially if the `COMPLETE` pragma were in the synonyms' defining module -- to check these declarations. Of course, GHC will issue false negatives (that is, say that a set is not complete when it actually is) but some checking is better than none. - How does this interact with GADTs? For example, load this code into your head: {{{ data G a where GInt :: G Int GBool :: G Bool pattern PInt :: forall a. () => a ~ Int => G a pattern PInt = GInt f1 :: G a -> () f1 GInt = () f2 :: G Int -> () f2 GInt = () f3 :: G Int -> () f3 PInt = () }}} By default, `f1` and `f3` will get incomplete match warnings, and `f2` does not. a. If I say `{-# COMPLETE GInt, GBool #-}`, does this change the default warning behavior? b. How can I have GHC notice that `f3` is a complete match? Saying `{-# COMPLETE PInt #-}` would seem disastrous. - What if multiple conflicting `COMPLETE` pragmas are in scope? For example, I have `{-# COMPLETE A, B #-}` and `{-# COMPLETE A #-}` in scope. Is a match over `A` complete? Is a warning/error issued about the pragmas? - The spec says "We verify that the result types of each constructor in a complete match agrees with each other." What does this sentence mean? Consider the possibility of pattern synonyms that match against functions, polymorphic patterns, and possibly even higher-rank patterns. I've not looked at all at the implementation, wanting to nail down the spec before considering any implementation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:44 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): To respond to an earlier point that Reid and others have made. The potential problems with this pragma only highlight design compromises with pattern synonyms. The specific issue being that pattern synonyms are ad- hoc collections rather than a complete set of covering patterns. Reid's suggestion of improving exhaustiveness checking by seeing if the view function is injective is akin to suggesting that one should only be allowed to define complete sets of pattern synonyms in the first place. I see the design I have implemented as the sensible way of doing so. If we forced all users to write pattern synonyms in the way that Reid described then we would have been better off implementing views! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:45 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Replying to [comment:44 goldfire]:
Somehow I've not looked at this thread, finding this only by a mention of `COMPLETE` elsewhere. (This is my fault -- just explaining my silence on this topic which is in my area of interest.)
A few nitpicks about the specification: - The wiki page uses "total" in several places, but I think you mean "covering". I use "total" to refer to functions that are both covering and terminating.
I agree with this.
- Would the following be acceptable?
{{{ data Void data T = T1 Int | T2 Bool | T3 Void {-# COMPLETE T1, T2 #-} }}}
It would seem so. I'm happy for this to be accepted; I'm just stress-testing the spec.
- The argument for not having the pattern-match checker look through
Yes. pattern synonyms is reasonable. But is there a way to have GHC do some checking on `COMPLETE` declarations? It would be great -- especially if the `COMPLETE` pragma were in the synonyms' defining module -- to check these declarations. Of course, GHC will issue false negatives (that is, say that a set is not complete when it actually is) but some checking is better than none. There are two problems with this I think. 1. If we allow `COMPLETE` pragmas in modules other than the definition module then we would have to include the RHS of a pattern synonym in the interface file. 2. In most instances, the checker will fail and produce a warning, and then what? The warning wouldn't be actionable in some way without another syntactic clue to tell the compiler to *really* trust us. It seems like a lot of effort.
- How does this interact with GADTs? For example, load this code into your head:
{{{ data G a where GInt :: G Int GBool :: G Bool
pattern PInt :: forall a. () => a ~ Int => G a pattern PInt = GInt
f1 :: G a -> () f1 GInt = ()
f2 :: G Int -> () f2 GInt = ()
f3 :: G Int -> () f3 PInt = () }}}
By default, `f1` and `f3` will get incomplete match warnings, and `f2` does not.
a. If I say `{-# COMPLETE GInt, GBool #-}`, does this change the default warning behavior?
With my latest changes, all else being equal we choose the error from the builtin set rather than any user specified set so the warnings will remain the same.
b. How can I have GHC notice that `f3` is a complete match? Saying
`{-# COMPLETE PInt #-}` would seem disastrous.
The correct thing to specify would be `{-# COMPLETE GBool, PInt #-}` and in that case, my implementation does not warn about `f3`.
- What if multiple conflicting `COMPLETE` pragmas are in scope? For example, I have `{-# COMPLETE A, B #-}` and `{-# COMPLETE A #-}` in scope. Is a match over `A` complete? Is a warning/error issued about the pragmas?
- The spec says "We verify that the result types of each constructor in a complete match agrees with each other." What does this sentence mean? Consider the possibility of pattern synonyms that match against functions,
This is a fair point. It would seem that the `A,B` pragma is redundant because `A` is a subset of `A, B` but it is possible for overlapping pragmas to make sense. For example, we could have two pattern synonyms for `Just`, `PJ1`, `PJ2` and then specify `{-# COMPLETE Nothing, PJ1 #-}` and `{-# COMPLETE Nothing, PJ2 #-}`. polymorphic patterns, and possibly even higher-rank patterns.
It means that we look at the result type of each conlike and then verify that the type constructor for each type is the same. In the case of a set containing polymorphic patterns, at least one pattern in the set must have a definite type or you must specify a type signature to fix the type for the whole set.
I've not looked at all at the implementation, wanting to nail down the spec before considering any implementation.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:46 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I feel like my suggestion, whatever it was, must have been misinterpreted... I'm concerned about situations in which there are no view patterns, at all. Take this scenario. I have a data type with a lot of `Either` fields {{{#!hs data T = T String (Either Int T) (Either Int T) (Either Int T) (Either Int T) }}} and I need to write a bunch of functions like {{{#!hs f (T s (Left _) (Left _) (Left n) (Right _)) = replicate n s f (T s (Left _) (Left n) (Right _) (Right _)) = replicate (n-1) s -- ... }}} It sure would be handy if I could define {{{#!hs pattern L <- Left _ pattern R <- Right _ }}} to condense the long left-hand sides. It just seems so obvious that I should be able to use a ''pattern synonym'' as a shorthand for a pattern, without having to go through extra contortions to appease the exhaustiveness checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:47 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
GHC understands that if `p1, ..., pn` are exhaustive patterns for the result type of `f`, then `f -> p1, ..., f -> pn` are exhaustive patterns for the input type of f. This to some extent solves the problem of mixing
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): I was specifically referring to the second bullet point at the end of comment:31 . patterns defined in different modules, as long as those patterns are defined in terms of the same "view functions". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:48 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Ah okay. But that doesn't require knowing anything at all about `f`. It just requires that you used the same `f` in all the equations, and then chose a covering family `p1, ..., pn` of patterns for its output. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:49 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): And just to say it explicitly, GHC understanding that really doesn't have anything to do with pattern synonyms at all. Even if you write a pattern match like {{{#!hs f (g -> True) = 1 f (g -> False) = 2 }}} the exhaustiveness checker thinks there are unmatched cases, but it should be able to see that there aren't. (And the desugarer already turns this into a `case` that evaluates `g` only once, so it really seems like the exhaustiveness checker ought to be able to handle this!) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:50 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Here's another example continuing the `Either` theme. Suppose I have a synonym {{{#!hs pattern LL <- Left (Left _) }}} and a function {{{#!hs f LL = 0 f (Left (Right x)) = x f (Right y)) = -y }}} How can I get the exhaustiveness checker to accept this program with `COMPLETE`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:51 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Reid wants the pattern-match completeness check to be able to "see through" the definition of a pattern synonym. That is, he wants the client of `LL` in comment:51 to be able to see that `LL` is no more than `(Left (Left _))`. But currently pattern synonyms are set up to exploit ''abstraction''. All the client knows is the type of `LL`; and the names and types of a matching and building function for it. We have no mechanism at all for exposing `LL`'s implementation in an interface file, to client modules. That's not quite true: we have the unfolding for `LL`'s matching function. So in certain cases, where `LL` is simple, the unfolding tells you all about it. But that's pretty fragile (it might change if `LL` got a bit bigger) and it's not information that is easy for the pattern-match overlap checker to exploit --- for example the unfolding of the matcher might be cluttered with stuff to do with re-boxing arguments that had been UNPACKed. I'm not arguing for a particular way forward here; just trying to explain why the context makes it hard to do what Reid wants. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:52 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
- The spec says "We verify that the result types of each constructor in a complete match agrees with each other." What does this sentence mean? Consider the possibility of pattern synonyms that match against functions,
It means that we look at the result type of each conlike and then verify
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:46 mpickering]: Thanks for this detailed reply! I'm happy with all your responses save one: polymorphic patterns, and possibly even higher-rank patterns. that the type constructor for each type is the same. In the case of a set containing polymorphic patterns, at least one pattern in the set must have a definite type or you must specify a type signature to fix the type for the whole set. I'm not sure what you mean here. Where do you specify the type signature? In the `COMPLETE` pragma? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:53 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Changes (by br1): * cc: br1 (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:54 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Replying to [comment:46 mpickering]:
Thanks for this detailed reply! I'm happy with all your responses save one:
- The spec says "We verify that the result types of each constructor in a complete match agrees with each other." What does this sentence mean? Consider the possibility of pattern synonyms that match against functions, polymorphic patterns, and possibly even higher-rank
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Replying to [comment:53 goldfire]: patterns.
It means that we look at the result type of each conlike and then verify that the type constructor for each type is the same. In the case of a set containing polymorphic patterns, at least one pattern in the set must have a definite type or you must specify a type signature to fix the type for the whole set.
I'm not sure what you mean here. Where do you specify the type signature? In the `COMPLETE` pragma?
I updated the wiki page now with lots of examples. You can specify something like.. {{{#!hs pattern P :: Maybe a pattern P = Nothing {-# COMPLETE P :: Maybe #-} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:55 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms
-------------------------------------+-------------------------------------
Reporter: nomeata | Owner: mpickering
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.8.1
checker) | Keywords:
Resolution: | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D2669
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Matthew Pickering
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: fixed | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:57 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8779: Exhaustiveness checks for pattern synonyms
-------------------------------------+-------------------------------------
Reporter: nomeata | Owner: mpickering
Type: feature request | Status: closed
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.8.1
checker) | Keywords:
Resolution: fixed | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D2669
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
participants (1)
-
GHC