This post shows how to use the Liar paradox to prove that that Haskell is inconsistent without using recursive terms.

We start with standard definitions of False and Not:

data False
type Not a = a -> False

Liar is an encoding of the Liar Paradox: "This sentence is false"

data Liar = Liar (Not Liar)

Note that Liar occurs in a negative position in the type of the constructor, so we cannot define Liar in consistent logics like Coq or Agda.

We can now create a proof of Not Liar by applying the proof contained in a Liar to itself:

honest :: Not Liar
honest l@(Liar p) = p l

Then we can easily prove False:

absurd :: False
absurd = honest $ Liar honest