Why does using PatternSynonyms trigger a non-exhaustive match warning?

Question

I'm following this answer to learn how to pattern match on Sequences. For concreteness, imagine that I'm implementing breadth-first search over a 2-d grid using a Sequence as a queue. Using just ViewPatterns, I might come up with something like the following:

{-# LANGUAGE ViewPatterns #-}

import qualified Data.Sequence as Seq
import qualified Data.Set as Set

bfs :: Seq.Seq ((Int, Int), Int) -> Set.Set (Int, Int) -> Int
bfs (Seq.viewr -> Seq.EmptyR) _ = -1 -- goal not found
bfs (Seq.viewr -> (coords Seq.:> (coord@(r, c), dist))) seen = -- search plumbing...

Following @Cactus's answer, if I also want to use PatternSynonyms, I come up with:

{-# LANGUAGE PatternSynonyms #-}

...

pattern Empty :: Seq.Seq a
pattern Empty <- (Seq.viewr -> Seq.EmptyR)

pattern (:>) :: Seq.Seq a -> a -> Seq.Seq a
pattern xs :> x <- (Seq.viewr -> xs Seq.:> x)

bfsPat :: Seq.Seq ((Int, Int), Int) -> Set.Set (Int, Int) -> Int
bfsPat Empty _ = -1
bfsPat (coords :> (coord@(r, c), dist)) seen = ...

These seem equivalent to me, but the compiler disagrees:

    In an equation for ‘bfsPat’:
        Patterns not matched:
            (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
            (Data.Set.Internal.Bin _ _ _ _)
            (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
            Data.Set.Internal.Tip
            (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
            (Data.Set.Internal.Bin _ _ _ _)
            (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
            Data.Set.Internal.Tip
            ...

What have I missed that breaks equivalence between these two formulations, and how can I fix it?

Aside, note that the answer you link is from 2015. Since `containers` 0.5.8 (2016), `Data.Sequence` has exported pattern synonyms bundled with the type, so you can use e.g. `Seq.Empty` and `import Data.Sequence (Seq ((:<|), (:|>)))`; version 0.5.10 (2018) added the proper `Complete` pragma. — Jon Purdy, Nov 22 '22 at 06:24

score 6 · Accepted Answer · edited Nov 22 '22 at 01:51

6

Check out the wiki page on COMPLETE pragmas. I'll quote the start: "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."

In short, you need to provide a COMPLETE pragma such as:

{-# COMPLETE Empty, (:>) #-}

edited Nov 22 '22 at 01:51

thisisrandy

2,660
2
12
25

answered Nov 22 '22 at 01:47

DDub

3,884
1
5
12

4

Probably worth mentioning that the compiler trusts you when you tell it what patterns are complete like this. If you lie to it, you won't get warnings at compile time but it will still blow up at runtime. – Joseph Sible-Reinstate Monica Nov 22 '22 at 01:50

Why does using PatternSynonyms trigger a non-exhaustive match warning?

1 Answers1

Linked