Opened 6 years ago

Last modified 3 years ago

#8779 closed feature request

Exhaustiveness checks for pattern synonyms — at Version 14

Reported by: nomeata Owned by:
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):
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 (14)

comment:1 Changed 6 years ago by merijn

Cc: merijn@… added

comment:2 Changed 6 years ago by dfranke

Cc: dfranke added

comment:3 Changed 6 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 5 years ago by cactus

Keywords: pattern synonyms added

comment:5 Changed 5 years ago by Artyom.Kazak

Cc: yom@… added

comment:6 Changed 5 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed

comment:7 Changed 5 years ago by cactus

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

comment:8 Changed 5 years ago by Feuerbach

Cc: roma@… added

comment:9 Changed 4 years ago by hvr

Version: 7.6.37.8.1

GHC 7.6 didn't support PatternSynonyms yet

comment:10 Changed 4 years ago by anders_

Cc: hello@… added

comment:11 Changed 4 years 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 4 years 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 4 years ago by bgamari

Cc: gkaracha added

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

comment:14 Changed 4 years ago by bgamari

Description: modified (diff)
Note: See TracTickets for help on using tickets.