Bang patterns don't work as the specification says

In investigating the behavior of bang patterns for an implementation of my own, I came across a discrepancy between the specification and GHC's implementation. Here is an example:

case Nothing of
  !(~(Just x)) -> 5
  Nothing      -> 12

This evaluates to 12. In other words, !(~p) is equivalent to p. However, the bang patterns description says that this should be equivalent to:

Nothing `seq` case Nothing of
  ~(Just x) -> 5
  Nothing   -> 12

which evaluates to 5. So, one of either the description or the implementation must be incorrect. In fact, GHC is even a bit confused, as it issues a warning about overlapping patterns for the bang pattern case statement, even though the successful branch is the 'unreachable' one.

The description makes more sense to me, but I'm not terribly invested in the behavior of this; it is admittedly a pretty obscure corner case.

Trac metadata

Trac field	Value
Version	7.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture