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

20 Sep 2017

      ...
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
#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#ErrorMess...
 here]. (Why is this not in the users' guide?) The relevant bit is:

 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