#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


 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 :==:

 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

Reply via email to