GHC diverges when proving nonequality of types

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

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information