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):

 One use case, GHC has a type

 {{{#!hs
 data GenLocated l e = L l e
 }}}

 It's common to see code where the location information is ignored `L _
 xxx`

 {{{#!hs
 -- data RuleBndr name
 --   = RuleBndr (Located name)
 --   | RuleBndrSig (Located name) (LHsSigWcType name)
 ...

   get_var (L _ (RuleBndrSig v _)) = v
   get_var (L _ (RuleBndr v)) = v
 }}}

 Ignoring whether it would be a worthwhile for GHC we define

 {{{#!hs
 {-# COMPLETE_PATTERNS LRuleBndr, LRuleBndrSig #-}
 pattern LRuleBndr    a   <- L _ (RuleBndr a)
 pattern LRuleBndrSig a b <- L _ (RuleBndrSig a b)
 }}}

 this becomes error prone for larger AST like `StmtLR`, especially when
 more cases get added

 {{{#!hs
 {-# COMPLETE_PATTERNS L_ #-}
 pattern L_ a <- L _ a

 {-# COMPLETE_PATTERNS
     LLastStmt,
     LBindStmt,
     LApplicativeStmt,
     (LLetStmt | LLetStmtL),  -- ?
     ...
 #-}
 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)
 pattern LBodyStmt        a b c d   <- L_ (BodyStmt        a b c d)
 pattern LLetStmt         a         <- L_ (LetStmt         a)
 pattern LLetStmtL        a         <- L_ (LetStmt (L_     a))
 ...
 }}}

 It is increasingly clear to me that ''some form'' of exhaustivity
 inference is needed, but that's all I've got.

 ----

 Do we allow mixing

 {{{#!hs
 {-# COMPLETE_PATTERNS None, Just | Nothing, Some | None, Some #-}
 pattern None   = Nothing
 pattern Some x = Just x
 }}}

 can this be inferred as exhaustive

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

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