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

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?

>Solution :

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, (:>) #-}