[GHC] #15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types

[GHC]

#15885: Enhancing COMPLETE pragma to support pattern synonyms with polymorphic
(output) types
-------------------------------------+-------------------------------------
        Reporter:  Shayan-Najd       |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings,
                                     |  PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by carter):

 reproducing my remarks from email

 off hand, once we're in in viewpattern/ pattern synonym land, ORDER of the
 abstracted constructors matters!

 consider

 `foo,bar,baz,quux,boom :: Nat -> String`

 plus some pattern synonyms i name "PowerOfTwo", "Even" and "Odd"

 {{{
 foo (PowerOfTwo x) = "power of two"
 foo (Even x) = "even"
 foo (Odd x) = "odd"

 bar (Even x) = "even"
 bar (Odd x) = "odd"

 baz (PowerOfTwo x) = "power of two"
 baz (Odd x) = "odd"

 quux (Even x) = "even"
 quux (Odd x) = "odd"
 quux (PowerOfTwo) = "power of two"

 boom (Even x) = "even"
 boom (PowerOfTwo x) = "power of two"
 boom (Odd x) = "odd"
 }}}

 `foo` and `bar` are both total definitions with unambiguous meanings, even
 though `bar`'s patterns are a suffix of `foos`!
 `baz` is partial!

 both boom and quux have a redudant overlapping case, power of two!

 so some thoughts

 1) order matters!
 2) pattern synonyms at type T are part of an infinite lattice, Top element
 == accept everything, Bottom element = reject everything

 3) `PowerOfTwo` <= `Even`  in the Lattice of patterns for `Natural`, both
 are "incomparable" with `Odd`

 4)
 {{{
 for a simple case on a single  value  at type T, assume c1 <= c2
                      , then  if   c1 x -> ... is before c2 x -> in the
 cases,
                     then both are useful/computationally meaningful / not
 irrelevant
                     OTHERWISE
                       when its  roughly
                   case x :: T of
                          c2 x -> ...
                          c1 x -> ...
 then the 'c1 x'  is redundant
 }}}

 this is slightly orthogonal to other facets of this discussion so far, but
 i realized that Richard's Set of Sets of patterns model misses some
 useful/ meaningful examples/extra structure from
 a) the implicit lattice of different patterns possibly being super/subsets
 (which is still something of an approximation, but with these example I
 shared above I hope i've sketched out some motivation )
 b) we can possibly model HOW ordering of clauses impacts coverage/totality
 / redundancy of clauses

 I'm not sure if it'd be pleasant/good from a user experience perspective
 to have this sort of partial ordering modelling stuff, but certainly seems
 like it would help distinguish some useful examples where the program
 meaning / coverage is sensitive to clause ordering

 i can try to spell this out more if theres interest, but I wanted to share
 while the iron was hot

 best!

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