GHC diverges when proving nonequality of types

Conor posted an interesting suggestion for proving type non-equality here:

http://www.nabble.com/Re%3A-Is-it-possible-to-prove-type-*non*-equality-in-Haskell--p25153135.html

I implemented it on my Nat framework and got GHC to diverge:

C:\haskell>ghc -c Absurd.hs
stack overflow: use +RTS -K<size> to increase it

I've attempted to shrink the code as much as possible and still reproduce the error; attached is the result.

Trac metadata

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