Re: [GHC] #8779: Exhaustiveness checks for pattern synonyms

7 Jun 2016

      #8779: Exhaustiveness checks for pattern synonyms
-------------------------------------+-------------------------------------
        Reporter:  nomeata           |                Owner:
            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):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 === Halfbaked thought
 Map to constructors whose exhaustivity information is known.

 {{{#!hs
 {-# PATTERN
     Empty     = EmptyL
     x  :<| xs = x :< xs
     xs :|> x  = x :< xs
 #-}
 pattern Empty    <- (Seq.viewl -> Seq.EmptyL)
 pattern x :<| xs <- (Seq.viewl -> x  :< xs)
 pattern xs :|> x <- (Seq.viewr -> xs :> x)
 }}}

 {{{#!hs
 {-# PATTERN
     None   = Nothing
     Some x = Just x
 #-}
 pattern None   = Nothing
 pattern Some x = Just x
 }}}

 {{{#!hs
 {-# PATTERN
     ErrorCall err = ErrorCallWithLocation err _
 #-}
 pattern ErrorCall err <- ErrorCallWithLocation err _
 }}}

 {{{#!hs
 {-# PATTERN
     LLastStmt        a b c     <- L _ (LastStmt        a b c)
     LBindStmt        a b c d e <- L _ (BindStmt        a b c d e)
     LApplicativeStmt a b c     <- L _ (ApplicativeStmt a b c)
     ...
 #-}
 pattern LLastStmt        a b c     <- L _ (LastStmt        a b c)
 pattern LBindStmt        a b c d e <- L _ (BindStmt        a b c d e)
 pattern LApplicativeStmt a b c     <- L _ (ApplicativeStmt a b c)
 ...
 }}}

 Then whenever the solver encounters

 {{{#!hs
 len Empty      = 0
 len (xs :|> _) = 1 + len xs
 }}}

 it is as if the user had written the exhaustive `len EmptyL = ...; len
 (_:<xs) = ...`.

 === What do we gain? ===
 The user can choose when to "break abstraction" (to mpickering's point),
 can mix constructors.

 {{{#!hs
 foo None   = ...
 foo Just{} = ...
 }}}

 === Problems ===
 {{{#!hs
 bar Empty         = ...
 bar (True  :<| _) = ...
 bar (_ :|> False) = ...
 }}}

 This results in a false positive

 {{{#!hs
 bar EmptyL       = ...
 bar (True  :< _) = ...
 bar (False :< _) = ...
 }}}

 idk

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