Pattern synonyms lead to unexhaustive pattern matching

Question

I've managed to construct the following "minimal" example that shows my problem.

Provided the PatternSynonyms extension is enabled

data Vec = Vec Int Int

pattern Ve x y = Vec x y

f :: (Vec, Vec) -> Vec
f (v@(Ve a b), Ve c d)
    | a > b     = Vec c d
    | otherwise = v

I get a warning for the function f saying

  Warning: Pattern match(es) are non-exhaustive
  In an equation for `f': Patterns not matched: (_, _)

If I replaced every Ve with Vec it wouldn't complain. How does my singular pattern synonym interfere here?

Answer 1

It is not implemented yet, see #8779. I'm not an expect here, but I know that exhaustiveness checks are hard to implement in a lot of cases, like GADT or guards. Probably it is problematic for pattern synonyms too.