#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