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

12 Aug 2015

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

Comment (by bgamari):

 == Proposal

 An `ImpossibleCases` language extension is introduced which turns
 `impossible`
 into a keyword when enabled. This keyword can be inserted in the place of
 a
 right-hand-side of an equation or case alternative to indicate that the
 left-hand-side pattern is ill-typed. This is useful for clarifying the
 meaning
 of the code to later readers as well as satisfying exhaustiveness warnings
 when
 the exhaustiveness check is unable to see that the pattern is ill-typed.

 To demonstrate this let's consider a standard dependently-typed vector,
 {{{#!hs
 data Vect (n::Nat) a where
     (:::) :: a -> Vect (n-1) a -> Vect n a
     Nil   :: Vect 0 a
 }}}

 Perhaps we want a `head` operation on this type (note that this is a toy
 example; GHC's exhaustiveness checker currently has no trouble identifying
 the
 `Nil` case as impossible). An equation would look something like,
 {{{#!hs
 head :: (KnownNat (n :: Nat)) => Vect (n+1) a -> a
 head Nil          impossible
 head (a:::_)    = a
 }}}

 A case analysis would look like,
 {{{#!hs
 head :: (KnownNat (n :: Nat)) => Vect (n+1) a -> a
 head x = case x of
            Nil       impossible
            a:::_  -> a
 }}}

 This could also be used in `LambdaCase` expressions,
 {{{#!hs
 head :: (KnownNat (n :: Nat)) => Vect (n+1) a -> a
 head = \case
           Nil        impossible
           a:::_   -> a
 }}}

 When the exhaustiveness checker sees a so-marked pattern it will suppress
 a
 missing-case warning.

 == Related Work

 As noted in the ticket description, the recent (and hopefully soon to be
 merged)
 [[http://research.microsoft.com/en-us/um/people/simonpj/papers/pattern-
 matching/gadtpm.pdf|GADT exhaustiveness]] work will reduce the need for
 these annotations, however this
 need will not be eliminated (see the Evaluation section of the paper).
 Moreover even with perfect exhaustiveness detection these annotations can
 elucidate complex pattern matches, making it explicit to the reader which
 cases he needn't worry about.

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