Pattern synonym exhaustiveness checks don't play well with EmptyCase

In #8779 (closed), mpickering added a COMPLETE pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with EmptyCase. Suppose I write

newtype Fin (n :: Nat) = Fin Natural  -- constructor not exported

pattern FZ :: () => n ~ 'S m => Fin n
pattern FS :: () => n ~ 'S m => Fin m -> Fin n
{-# COMPLETE FZ, FS #-}

I would very much like to be able to write

finZAbsurd :: Fin 'Z -> Void
finZAbsurd x = case x of

but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this:

When checking empty case, check that at least one complete pattern set is impossible.

In this case, it would see two complete pattern sets: the built-in {Fin} and the user-decreed {FZ, FS}. Since neither FZ nor FS have matching types, we should conclude that the empty case is fine.