[GHC] #10756: Allow users to indicate inaccessible patterns

[GHC]

#10756: Allow users to indicate inaccessible patterns
-------------------------------------+-------------------------------------
              Reporter:  edsko       |             Owner:
                  Type:  feature     |            Status:  new
  request                            |
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.2
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Consider

 {{{#!hs
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GADTs          #-}

 data Elem :: * -> * -> * where
   EZ :: Elem (f , fs) f
   ES :: Elem fs f -> Elem (f', fs) f

 elemAbsurd :: Elem () f -> a
 elemAbsurd _ = error "inaccessible"
 }}}

 This catch-all in `elemAbsurd` is very unfortunate, because if I change my
 datatype and not all cases are inaccessible anymore the type checker will
 not be warning me. Although of course there is recent work by SPJ et al on
 inferring more inaccessible cases, I think it would be tremendously useful
 for users to be able to indicate that patterns are in fact inaccesible.
 I'd be very happy if I could write

 {{{#!hs
 elemAbsurd :: Elem () f -> a
 elemAbsurd EZ     = inaccessible
 elemAbsurd (ES _) = inaccessible
 }}}

 Note that ghc ''can already detect that these patterns are in fact
 inaccessible'': it won't let me write the above:

 {{{
 T.hs:12:12:
     Couldn't match type ‘()’ with ‘(f, fs)’
     Inaccessible code in
       a pattern with constructor
         EZ :: forall f fs. Elem (f, fs) f,
       in an equation for ‘elemAbsurd’
 }}}

 So I think it should be very very simple to change the type checker to
 allow to write cases like this if and only if the RHS is a specially
 designated symbol "inaccessible", which could be defined simply as

 {{{#!hs
 inaccessible :: a
 inaccessible = error "inaccessible"
 }}}

 in `GHC.Prim` or something. This would seem like very little work, and a
 correspondingly tiny patch, but with quite a large payoff.

 Future work in automatically detecting inaccessible cases would not make
 existing code using this style wrong, it just means that we have to write
 fewer inaccessible cases by hand; but even with more sophisticated
 inference algorithms for inaccessible cases there will still be
 inaccessible cases remaining.

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