Allow users to indicate inaccessible patterns

Consider

{-# 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

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

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.

Trac metadata

Trac field	Value
Version	7.10.2
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture