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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information