Allow empty case analysis

Using -XEmptyDataDecls I can declare an (almost) empty data type.

  data Void

However, I can't use an empty case to discriminate values of the empty type.

This does not work:

  get :: Void -> a

Only the type signature, but no body. [This would be useful also in other circumstances.]

  get :: Void -> a
  get v = case v of { }

An empty case in the body.

changed weight to 5

added Tfeature request Trac import labels

changed the description

Why is this useful? The only value of type Void is bottom.

Simon

This would be somewhat useful for the Derive tool (http://www.cs.york.ac.uk/fp/darcs/derive), and in general for program generation. Consider the automatically derived instance for Show, on an empty data type. What you are likely to get is:

instance Show Void where

i.e. the complete absense of anything. If you changed the generator to make a case statement, you could get:

instance Show Void where
    show x = case x of {}

Which is a more accurate reflection of what was intended, and I think the point Ralf is trying to make. Derive probably goes wrong with empty data types, but if it didn't, this extension would be helpful.

I tried to construct an empty case with Template Haskell, and crashed GHC:

C:\Neil\Temp>ghci -fth
GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> :m Language.Haskell.TH
Prelude Language.Haskell.TH> $(caseE (litE $ CharL 'a') [])
: panic! (the 'impossible' happened)
  (GHC version 6.8.2 for i386-unknown-mingw32):
        readFilledBox t_a1b5{tv} [box]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Of course, with the correct warning flags enabled, empty case of a non-empty type will produce an "incomplete pattern match" warning: exactly when we want a warning for using this construct.

I suppose the effect is to throw a pattern-match error that is independent of the case'd value, as consistent with all patterns of any other case statement failing? (rather than using it if it's |, as of course it will be if it's an empty type: because, unlike in GHC Core, source-Haskell 'case' does not introduce strictness)

+1, I've occasionally wanted this to be possible

changed milestone to %6.12 branch

Perhaps this would be better proposed for Haskell'?

removed milestone

changed weight to 3

OK so I don't like GHC crashing, ever, so I have done the following:

• In the renamer and typechecker, I allow empty HsCase.
• In Core I still don't allow empty Case. I have no idea what stuff would break if empty Case was allowed; but even finding the type of an expression might become impossible. (Yes, at the moment Case records its result type, but with the new FC stuff that's not necessary and I may remove it.) And I see no reason to support it.
• In the desugarer, I desguar empty HsCase to a call to error. (The simplifier already does this if it can figure out that a case is empty; see Simplify.rebuildCase.)

So now Neil's TH example works instead of crashing. The parser prevents you doing this in source code, so I have not added a flag.

To go the full distance we still need:

• Parser to accept empty case expressions (currently rejected by parser)
• -X flag to control this language extension
• Test somewhere (in renamer) to check that empty case only happens when flag is on.
• User manual docs
• Regresssion tests in test suite.

All easy but tiresome. If you care about this, send a patch! I've done the slightly-tricky bits. So I'll leave this bug open at low priority, milestone bottom.

Simon

Trac metadata

Trac field	Value
Priority	normal → low

mentioned in commit 27de38ef

mentioned in commit abc0aac6

Replying to [#2431 (closed) malcolm.wallace@cs.york.ac.uk]:

I tried to think of how parsing might go wrong. Consider the following (contrived) example:

case foo of
[] ->
case bar of
(x:xs) ->
baz

Did you spot that the second alternative is indented with a tab rather than spaces, (with editor tab width set to 2 instead of 8)?

I realise the example is contrived, but I don't think we need to consider it. The Haskell report defines tab stops to be 8 characters apart, so you should always have your editor set to use 8-character tab stops when editing Haskell code, because that's how the compiler sees it. Anything else will cause confusion, in many more ways than just the example above. If you don't like 8-char tabs then fine: use spaces instead, and -fwarn-tabs, but you should still set your editor to use 8-char tabs so that you can read other people's code.

Trac metadata

Trac field	Value
Architecture	Unknown → Unknown/Multiple

Trac metadata

Trac field	Value
Operating system	Unknown → Unknown/Multiple

mentioned in issue #5340 (closed)

mentioned in issue #6067 (closed)

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 (closed). But, once that is fixed, empty pattern matches would have a new lease on life.

Trac metadata

Trac field	Value
TypeOfFailure	- → OtherFailure
CC	id@isaac.cedarswampstudios.org → eir@cis.upenn.edu, id@isaac.cedarswampstudios.org

changed title from allow empty case analysis to Allow empty case analysis