Opened 4 years ago

Closed 9 months ago

Last modified 8 months ago

#8779 closed feature request (fixed)

Exhaustiveness checks for pattern synonyms

Reported by: nomeata Owned by: mpickering
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.1
Keywords: PatternSynonyms Cc: lelf, ekmett, roma@…, yom@…, cactus, merijn@…, dfranke, hello@…, mpickering, gkaracha, liyang, Iceland_jack, dfeuer, akio, hesselink, mgsloan, RyanGlScott, br1
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:

Description (last modified by bgamari)

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.

Change History (58)

comment:1 Changed 3 years ago by merijn

Cc: merijn@… added

comment:2 Changed 3 years ago by dfranke

Cc: dfranke added

comment:3 Changed 3 years ago 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.

comment:4 Changed 3 years ago by cactus

Keywords: pattern synonyms added

comment:5 Changed 3 years ago by Artyom.Kazak

Cc: yom@… added

comment:6 Changed 3 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed

comment:7 Changed 3 years ago by cactus

Just thinking out loud here, but does the PatternMatchCheck story have something to offer us here?

comment:8 Changed 3 years ago by Feuerbach

Cc: roma@… added

comment:9 Changed 2 years ago by hvr

Version: 7.6.37.8.1

GHC 7.6 didn't support PatternSynonyms yet

comment:10 Changed 23 months ago by anders_

Cc: hello@… added

comment:11 Changed 23 months ago by mpickering

Cc: mpickering added

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.

comment:12 Changed 22 months ago by hvr

I just stumbled over an annoying case due to our new ErrorCall in GHC 8.0:

{-# 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: _

comment:13 Changed 22 months ago by bgamari

Cc: gkaracha added

CCing George Karachalias, who is responsible for our greatly improved new exhaustiveness checker.

comment:14 Changed 22 months ago by bgamari

Description: modified (diff)

comment:15 Changed 19 months ago by liyang

Cc: liyang added

comment:16 Changed 19 months ago by Iceland_jack

Cc: Iceland_jack added

comment:17 Changed 18 months ago by dfeuer

Cc: dfeuer added

I suspect making this really work right may require some modifications to the pattern synonym concept. For example,

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.

comment:18 Changed 18 months ago by dfeuer

Oh, I see that was proposed initially. Duh!

comment:19 Changed 18 months ago by akio

Cc: akio added

comment:20 Changed 18 months ago by hesselink

Cc: hesselink added

comment:21 Changed 17 months ago by mgsloan

Cc: mgsloan added

+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

comment:22 Changed 17 months ago by Iceland_jack

Here's a crazy idea, associate every pattern synonym with a (edit: view) data type (this could also be a new ‘form’ of pattern synonyms).

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

comment:23 in reply to:  22 ; Changed 17 months ago by dfeuer

Replying to 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.

comment:24 in reply to:  23 Changed 17 months ago by Iceland_jack

Replying to 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

{-# MINIMAL fromRational, (recip | (/)) #-}

If you want to express that Empty and (:<|) form a complete pattern but so does Empty and (:|>)

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

what's stopping us from writing

{-# COMPLETE_PATTERNS (Empty, (:<|)) | (Empty, (:|>)) #-}

to mean just that?

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

comment:25 Changed 17 months ago 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

{-# COMPLETE_PATTERNS Empty, (:<|) #-}
{-# COMPLETE_PATTERNS Empty, (:|>) #-}

would equal what I proposed (if I got the precedence right)

{-# 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 users guide:

If no MINIMAL pragma is given in the class declaration, it is just as if a pragma

{-# MINIMAL op1, op2, ..., opn #-} 

was given, where the opi are the methods

  1. that lack a default method in the class declaration, and
  2. 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

data ABC = A | B | C 

it is as if the she had also written {-# COMPLETE_PATTERNS A, B, C #-}. Would this work with GADTs?

comment:26 Changed 17 months ago by Iceland_jack

Unlike MINIMAL the patterns Empty, (:<|), (:|>) may be defined in separate modules.

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

comment:27 Changed 17 months ago by RyanGlScott

Cc: RyanGlScott added

comment:28 Changed 17 months ago by ekmett

Cc: ekmett added

comment:29 Changed 17 months ago by Iceland_jack

One use case, GHC has a type

data GenLocated l e = L l e

It's common to see code where the location information is ignored L _ xxx

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

{-# 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

{-# 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

{-# COMPLETE_PATTERNS None, Just | Nothing, Some | None, Some #-}
pattern None   = Nothing
pattern Some x = Just x

can this be inferred as exhaustive

-- data ErrorCall = ErrorCallWithLocation String String
pattern ErrorCall err <- ErrorCallWithLocation err _

comment:30 Changed 17 months ago by Iceland_jack

Halfbaked thought

Map to constructors whose exhaustivity information is known.

{-# 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)
{-# PATTERN 
    None   = Nothing
    Some x = Just x
#-}
pattern None   = Nothing
pattern Some x = Just x
{-# PATTERN 
    ErrorCall err = ErrorCallWithLocation err _
#-}
pattern ErrorCall err <- ErrorCallWithLocation err _
{-# 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

len Empty      = 0
len (xs :|> _) = 1 + len xs

it is as if the user had written the exhaustive len EmptyL = ...; len (_:<xs) = ....

What do we gain?

The user can choose when to "break abstraction" (to mpickering's point), can mix constructors.

foo None   = ...
foo Just{} = ...

Problems

bar Empty         = ...
bar (True  :<| _) = ...
bar (_ :|> False) = ...

This results in a false positive

bar EmptyL       = ...
bar (True  :< _) = ...
bar (False :< _) = ...

idk

comment:31 Changed 17 months ago 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.

comment:32 Changed 17 months ago 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.

comment:33 Changed 17 months ago 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.

comment:34 Changed 17 months ago 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 Commands 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"

comment:35 Changed 17 months ago 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).

comment:36 Changed 12 months ago by mpickering

Owner: set to mpickering

comment:37 Changed 12 months ago by rwbarton

I still hope you're not planning to implement COMPLETE_PATTERNS :)

comment:38 Changed 11 months ago by mpickering

Differential Rev(s): Phab:D2669

comment:39 Changed 11 months ago 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

comment:40 Changed 11 months ago 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)

comment:41 Changed 11 months ago 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.

comment:42 Changed 11 months ago 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.

comment:43 Changed 11 months ago by lelf

Cc: lelf added

comment:44 Changed 10 months ago 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.

  1. If I say {-# COMPLETE GInt, GBool #-}, does this change the default warning behavior?
  1. 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.

comment:45 Changed 10 months ago 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!

comment:46 in reply to:  44 ; Changed 10 months ago by mpickering

Replying to 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.

Yes.

  • 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.

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.

  1. 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.

  1. 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?

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 #-}.

  • 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.

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.

comment:47 Changed 10 months ago 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

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

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

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.

comment:48 Changed 10 months ago by mpickering

I was specifically referring to the second bullet point at the end of comment:31 .

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".

comment:49 Changed 10 months ago 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.

comment:50 Changed 10 months ago 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

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

comment:51 Changed 10 months ago by rwbarton

Here's another example continuing the Either theme. Suppose I have a synonym

pattern LL <- Left (Left _)

and a function

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?

comment:52 Changed 9 months ago 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

comment:53 in reply to:  46 ; Changed 9 months ago by goldfire

Replying to 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 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?

comment:54 Changed 9 months ago by br1

Cc: br1 added

comment:55 in reply to:  53 Changed 9 months ago by mpickering

Replying to goldfire:

Replying to 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 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..

pattern P :: Maybe a
pattern P = Nothing

{-# COMPLETE P :: Maybe #-}

comment:56 Changed 9 months ago by Matthew Pickering <matthewtpickering@…>

In 1a3f1ee/ghc:

COMPLETE pragmas for enhanced pattern exhaustiveness checking

This patch adds a new pragma so that users can specify `COMPLETE` sets of
`ConLike`s in order to sate the pattern match checker.

A function which matches on all the patterns in a complete grouping
will not cause the exhaustiveness checker to emit warnings.

```
pattern P :: ()
pattern P = ()

{-# COMPLETE P #-}

foo P = ()
```

This example would previously have caused the checker to warn that
all cases were not matched even though matching on `P` is sufficient to
make `foo` covering. With the addition of the pragma, the compiler
will recognise that matching on `P` alone is enough and not emit
any warnings.

Reviewers: goldfire, gkaracha, alanz, austin, bgamari

Reviewed By: alanz

Subscribers: lelf, nomeata, gkaracha, thomie

Differential Revision: https://phabricator.haskell.org/D2669

GHC Trac Issues: #8779

comment:57 Changed 9 months ago by mpickering

Resolution: fixed
Status: newclosed

comment:58 Changed 8 months ago by Ben Gamari <ben@…>

In 122c6776/ghc:

Add COMPLETE pragmas for TypeRep and ErrorCall pattern synonyms

When programming with the pattern synonyms for `TypeRep`, I noticed that
I was receiving spurious non-exhaustive pattern-match warnings.  This
can be easily fixed by adding `COMPLETE` pragmas for them.

Moreover, there's another pattern synonym in `base`: `ErrorCall`. In
fact, in the original ticket for `COMPLETE` pragmas (#8779), someone
requested that `ErrorCall` be given a `COMPLETE` pragma as well
(https://ghc.haskell.org/trac/ghc/ticket/8779#comment:21).  I decided to
do that as well while I was in town.

Reviewers: bgamari, mpickering, austin, hvr

Reviewed By: bgamari

Subscribers: rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3231
Note: See TracTickets for help on using tickets.