A proof of Löb's theorem in Haskell

Interesting to see you can jam something like this into Haskell despite its inappropriateness. The (genuine) Agda proofs are much, much nicer.