[GHC] #10756: Allow users to indicate inaccessible patterns
GHC
ghc-devs at haskell.org
Wed Aug 12 09:34:07 UTC 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
More information about the ghc-tickets
mailing list