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.