The key is that you can (in theory, I don't know if Haskell has a proper bottom that can act as a type) give a value of Void/Bottom to anything, analogous to lo

The key is that you can (in theory, I don't know if Haskell has a proper bottom that can act as a type) give a value of Void/Bottom to anything, analogous to logic in that a proof of nonsense can be used as a proof of anything. Take this Haskell code that passes the type checker: bottom = bottom f :: Int -> a f _ = bottom Here 'bottom' has the conceptual type Void/Bottom and checks successfully against the 'a'. So assuming we have this Void type in Haskell (I don't know if Haskell has it or not), this should also type check: f :: Void -> a f x = x Just like bottom (of type Void) checked against the 'a' earlier, an argument of that type should also type check.