The Haskell Elephant in the Room(stephendiehl.com)

  const absurd = <A>(): A => absurd()

  const unimplemented = <A>(): A => { throw new Error(“Unimplemented”) }

  const uninhabited: string & number = absurd()

    {-# LANGUAGE GADTs, TypeFamilies #-}

    -- Peano arithmetic: these types represent '0' and '1+n'
    data Zero
    data Succ n

    -- We can define 1 as '1+0', 2 as '1+1', and so on
    type Zero
    type Two = Succ One

    -- A closed type family is a function at the type level.
    -- This function implements addition of the above Peano numbers.
    type family Add x y where
      Add Zero     y = y
      Add (Succ x) y = Succ (Add x y)

    -- 'Equal a b' is a proof that types 'a' and 'b' are the same.
    -- It works by forcing the type variable 'x' in 'Refl' to unify with both.
    data Equal a b where
      Refl :: Equal x x

    -- The type checker will accept this proof that 1 + 1 = 2, giving:
    -- >[1 of 1] Compiling Main
    -- Ok, one module loaded.
    truePositive :: Equal (Add One One) Two
    truePositive = Refl

    -- The type checker will reject this proof that 1 + 1 = 1, giving:
    -- >[1 of 1] Compiling Main
    -- x.hs:24:16: error:
    --  • Couldn't match type ‘Zero’ with ‘Succ Zero’
    --    Expected type: Equal (Add One One) One
    --  Actual type: Equal One One
    --  • In the expression: Refl
    --  In an equation for ‘trueNegative’: trueNegative = Refl
    --     |
    --  24 | trueNegative = Refl
    --     |
    --trueNegative :: Equal (Add One One) One
    --trueNegative = Refl

    -- However, the type checker will accept this (unsound) proof
    -- that 1 + 1 = 1, giving:
    -- >[1 of 1] Compiling Main             ( x.hs, interpreted )
    -- Ok, one module loaded.
    falsePositive :: Equal (Add One One) One
    falsePositive = falsePositive

    loop :: forall a. a
    loop = loop