#2431: Allow empty case analysis
------------------------------------+---------------------------------------
Reporter: RalfHinze | Owner:
Type: feature request | Status: new
Priority: low | Milestone: _|_
Component: Compiler | Version: 6.8.3
Keywords: empty case analysis | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------------+---------------------------------------
Comment(by simonpj):
I didn't find the above entirely clear, so Richard elaborates: consider:
{{{
data a :~: b where
Refl :: a :~: a
absurd :: True :~: False -> a
}}}
Now, I want to write a term binding for `absurd`. Here are two candidates:
{{{
absurd x = error "absurd" -- (A)
absurd x = case x of {} -- (B)
}}}
I much prefer (B). Why? Because GHC can figure out that `(True :~:
False)` is an empty type. So (B) has no partiality and, (if #3927 is
fixed) I should be able to compile with `-fwarn-incomplete-patterns` and
`-Werror`.
On the other hand (A) looks dangerous, and GHC doesn't check to make sure
that, in fact, the function can never get called.
The bottom line, for me at least, is that I want to avoid the partial
constructs (incomplete patterns, undefined, etc) in Haskell as much as
possible, especially when I'm leveraging the type system to a high degree.
The lack of empty case statements forces me to use undefined where it
isn't really necessary.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2431#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
