[GHC] #14253: Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable

[GHC]

#14253: Pattern match checker mistakenly concludes pattern match on pattern synonym
is unreachable
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms,
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Regardless of the example's moral integrity, I posit that it exhibits
 buggy behavior.

 First, let's try to hammer out what //should// happen here. There's
 something of a specification buried in the annals of the GHC wiki
 [https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs#ErrorMessages
 here]. (Why is this not in the users' guide?) The relevant bit is:

 > When the pattern match checker requests a set of constructors for a type
 constructor `T`, we now return a list of sets which include the normal
 data constructor set and also any `COMPLETE` pragmas of type `T`. We then
 try each of these sets, not warning if any of them are a perfect match. In
 the case the match isn't perfect, we select one of the branches of the
 search depending on how good the result is.
 >
 > The results are prioritised in this order.
 >
 > 1. Fewest uncovered clauses
 > 2. Fewest redundant clauses
 > 3. Fewest inaccessible clauses
 > 4. Whether the match comes from a `COMPLETE` pragma or the built-in set
 of data constructors for a type constructor.

 In the example above, we're matching on something of type `T`, so we have
 the built-in constructor set `{MkT1, MkT2}` as well as the `COMPLETE` set
 `{MkT1}`. Since `u` only matches on `MkT2'`, the latter set `{MkT1}` (the
 `COMPLETE` set) has the fewest number of uncovered clauses, so we use that
 for reporting warnings. Therefore, the error that we would //expect// to
 get (but don't, due to this bug) is:

 {{{
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns not matched: MkT1
 }}}

 Does that sound agreeable?

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14253#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler