#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Reid wants the pattern-match completeness check to be able to "see through" the definition of a pattern synonym. That is, he wants the client of `LL` in comment:51 to be able to see that `LL` is no more than `(Left (Left _))`. But currently pattern synonyms are set up to exploit ''abstraction''. All the client knows is the type of `LL`; and the names and types of a matching and building function for it. We have no mechanism at all for exposing `LL`'s implementation in an interface file, to client modules. That's not quite true: we have the unfolding for `LL`'s matching function. So in certain cases, where `LL` is simple, the unfolding tells you all about it. But that's pretty fragile (it might change if `LL` got a bit bigger) and it's not information that is easy for the pattern-match overlap checker to exploit --- for example the unfolding of the matcher might be cluttered with stuff to do with re-boxing arguments that had been UNPACKed. I'm not arguing for a particular way forward here; just trying to explain why the context makes it hard to do what Reid wants. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:52 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler