Opened 10 months ago

Closed 10 months ago

Last modified 10 months ago

#15886 closed bug (invalid)

Spurious warning about incomplete pattern with PatternSynonyms

Reported by: selinger Owned by:
Priority: normal Milestone: 8.6.3
Component: Compiler Version: 8.6.1
Keywords: PatternSynonyms, PatternMatchWarnings Cc:
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}

module Test where

f :: Int -> Bool
f (id -> a) = True

pattern X a <- (id -> a)

g :: Int -> Bool
g (X a) = True

When compiling with -Wincomplete-patterns, this code produces an (incorrect) warning for g, but not for f. The only difference is that g uses a pattern synonym.

K.hs:12:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘g’: Patterns not matched: _
   |
12 | g (X a) = True
   | ^^^^^^^^^^^^^^

Change History (5)

comment:1 Changed 10 months ago by RyanGlScott

Keywords: PatternSynonyms PatternMatchWarnings added
Resolution: invalid
Status: newclosed

This is expected behavior. Refer to the users' guide section on COMPLETE sets:

The COMPLETE pragma is used to inform the pattern match checker that a certain set of patterns is complete and that any function which matches on all the specified patterns is total.

The most common usage of COMPLETE pragmas is with Pattern synonyms. On its own, the checker is very naive and assumes that any match involving a pattern synonym will fail. As a result, any pattern match on a pattern synonym is regarded as incomplete unless the user adds a catch-all case.

As this suggests, you need to declare a COMPLETE set for X in order for the coverage checker to reason about it. This variant of your program, for instance, does not emit any warnings when compiled with -Wincomplete-patterns:

{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}

module Test where

f :: Int -> Bool
f (id -> a) = True

pattern X a <- (id -> a)
{-# COMPLETE X :: Int #-}

g :: Int -> Bool
g (X a) = True

comment:2 Changed 10 months ago by selinger

Interesting. Thanks for pointing this out. I assumed (wrongly, it turns out) that since pattern synonyms are just syntactic sugar, the checker could desugar it for the purposes of coverage checking. Are there good reasons for "the checker is very naive"?

For sure, there are good uses cases for COMPLETE pragmas, because there are cases (even without using pattern synonyms) that's aren't readily decidable. I'm just surprised that the checker can't solve obvious cases.

comment:3 Changed 10 months ago by RyanGlScott

The rationale for requiring COMPLETE signatures to coverage-check pattern synonyms can be found in the corresponding GHC wiki page:

The exhaustiveness checker currently chokes on pattern synonyms. They are marked as always fallible patterns which means that we must also always include a catch-all case in order to avoid a warning.

data A = A

pattern :: A
pattern P = A

foo :: A -> A
foo P = A

leads to the warning that pattern matches for foo are non-exhaustive.

simpletest.hs:7:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘foo’: Patterns not matched: _

Inspecting the definition of P we can see that the matches for foo are indeed exhaustive as A is a unary data type but the pattern match checker does not make use of this information.

And neither should it! Pattern synonyms are a means of *abstraction*, if the exhaustiveness checker could look through a definition then the implementation of P would leak into error messages. We want users to be able to replace bona-fide data constructors with pattern synonyms without consumers noticing. To that end, we allow users to specify a complete set of pattern synonyms in order to sate the pattern match checker. If a complete pragma is not provided then we keep the same behaviour as in previous releases.

comment:4 Changed 10 months ago by selinger

OK, this makes sense. Thanks!

comment:5 Changed 10 months ago by goldfire

Is it worth pondering the utility of inferring a COMPLETE for an obviously-total pattern synonym? That is, GHC looks at the patsyn definition, sees that it's total (by doing its normal pattern-match completeness check) and then marks the patsyn as complete. This doesn't violate abstraction -- it's just a little more inference magic.

Indeed, this idea could be expanded, allowing you to tell GHC that you expect a certain set of pattern synonyms to be complete, asking GHC to check for you. For example:

patterns where   -- silly hypothetical syntax
  Some x = Just x
  None = Nothing

GHC would check these, notice that they're complete, and then pretend as if someone had said {-# COMPLETE Some, None #-}. If they're not complete, and we're warning about patterns, then issue a warning.

I don't care enough about this to write, defend, etc., a proposal on the subject, but perhaps you (for any value of "you") do.

Note: See TracTickets for help on using tickets.