Not really an answer but if you check out provability section of https://en.wikipedia.org/wiki/Löb's_theorem you'll find a formula very similiar to the haskell type, together with a proof in modal logic.