For functions types, there is only one equivalence class, because there is only one way to pattern-match a function. Observe that two elements can be distinguished by a set of patterns if and only if there is one element in the pattern set that already distinguishes them. Do pattern synonyms refine the equivalence relation induced by ordinary constructors? No.

What I said is only true in the absence of view patterns. With view patterns, a pattern match is no longer guaranteed to terminate, since the viewing function could diverge on the value being matched. Consider -- diverges on infinite lists end :: [a] -> [a] end xs = case tl xs of [] -> [] (_:xs') -> end xs' pattern Finite <- (end -> []) isFinite :: [a] -> Bool isFinite xs = case xs of Finite -> True _ -> False Notice that isFinite is no longer a clopen but an open: It either returns True or diverges. Moreover, view patterns introduce fine- grained clopens on function spaces, like pattern Q <- (($ 4) -> 3) We must conclude that in the presence of the ViewPatterns extension, the equivalenve relation induced by pattern matching is: "x~y whenever there is no function v and no pattern P such that (v x) and (v y) can be distinguished by P." It should not be hard to prove that deciding coverage by view patterns such as Finite would solve the halting problem.  Olaf