#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: |
------------------------------------+---------------------------------------
Changes (by goldfire):
* cc: eir@… (added)
* failure: => None/Unknown
Comment:
Now that GHC is getting more dependently typed features, an empty case
seems more useful. For example, I would like to define the following:
{{{
data a :==: b where
Refl :: a :==: a
data EmptySet
type Not a = a -> EmptySet
type DecidableEquality (a :: k) (b :: k) = Either (a :==: b) (Not (a :==:
b))
data SBool :: Bool -> * where
SFalse :: SBool False
STrue :: SBool True
eqBoolDec :: SBool a -> SBool b -> DecidableEquality a b
eqBoolDec SFalse SFalse = Left Refl
eqBoolDec STrue STrue = Left Refl
eqBoolDec SFalse STrue = Right (\case {})
eqBoolDec STrue SFalse = Right (\case {})
}}}
Even if empty pattern matches were allowed, I recognize that this would
just produce an (erroneous) incomplete pattern match warning, because of
bug #3927. But, once that is fixed, empty pattern matches would have a new
lease on life.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2431#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
