Haskell's type system is unsound. Here's an example, where we can prove that 1 + 1 = 1:
{-# 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 One = Succ 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
The unsound proof works because our type 'Equal a b' doesn't
only contain proofs that a = b (AKA 'Refl'); it
also contains infinite loops, like 'falsePositive = falsePositive' (AKA "bottom"). We can use this to undermine any guarantee we try to enforce using Haskell's type system. In fact, we can make a generic version, which can be used to satisfy any type constraint:
loop :: forall a. a
loop = loop
In theory, any time we actually try to use 'loop' our program will freeze; so we might think we're safe from any bad consequences; e.g. if we have 'launchTheMissiles :: PresidentialApproval -> IO ()' we can trick it with 'launchTheMissiles loop', but we're safe since that program contains an infinite loop, right?
Wrong! Haskell is lazy, so it won't bother evaluating arguments which aren't needed. Even if we try forcing the value, we can't be sure that the compiler won't optimise it away! In practice this means that we can't rely on the mere existence of well-typed values as proof of their types; we can be sure that our data dependencies exist (i.e. those values which are forced as part of our computation, which can't be optimised away), but we still won't know that beforehand (i.e. the program may crash or freeze at any point before a particular expression, due to the presence of "bottom" somewhere).