Empty case analysis for function clauses

Thanks to -XEmptyCase, the following is legal:

  module Empty where
  
  data Empty
  
  empty :: Empty -> a
  empty x = case x of { }

However, if I leave off the last line, GHC will complain that The type signature for ‘empty’ lacks an accompanying binding.

I think this program should be accepted. It isn't that I'm not giving a definition for empty; it's that I'm defining it to be a function with no accompanying equations, as could be represented in Template Haskell by

$(return [FunD (mkName "empty") []])

Currently, this too is rejected, with GHC complaining Function binding for ‘empty’ has no equations. I think this should be legal, with an empty list of clauses in a function definition being treated the same way as an empty list of matches in a case expression.

changed weight to 3

added Tfeature request Trac import labels

changed the description

But empty does have one case, where x = undefined. You can't pattern match on it but it's there.

I imagine that this is in attempt to simulate : ∀ α. ⊥ → α where we use the impossible pattern in empty but that's just not the case in Haskell and even in Agda &c the binding is necessary anyway.

Tricky. I believe the The type signature for ‘empty’ lacks an accompanying binding. message is emitted early, possibly during renaming, when there is no way to know that Empty is empty. Or are you suggesting to disable this error message completely when EmptyCase is active?

And what’s wrong with writing empty x = case x of { }?

Yes, with EmptyCase active I would take any type declaration without an accompanying binding as denoting an empty definition, and then issue a warning about an inexhaustive pattern match later on when appropriate.

Having to write the empty case expression doesn't prevent you from doing anything. It just adds clutter, and allowing empty case analysis in some syntactic contexts but not others is an unnecessary inconsistency.

A somewhat similar discussion took place in #11390 (closed).

Trac metadata

Trac field	Value
Related	- → #11390 (closed)

added Plow label