There's only one Leibniz


Leibniz's characterisation of what it means for AA to equal BB is that if P(A)P(A) holds for any property PP, then so does P(B)P(B). In other words, equality is the relation that allows substitution of BB for AA in any context.

There can only be one reflexive relation with this substitution property. If we have two substitutive reflexive relations \sim and \simeq, then as soon as ABA \sim B we can substitute the second occurrence of AA for BB in AAA \simeq A, so necessarily ABA \simeq B too.

Haskell1 had a soundness issue that arose from trying to have two distinct equality-like relations2. Haskell supports newtype, a mechanism for creating a new copy TT' of a previously-defined type TT, and the GeneralizedNewtypeDeriving mechanism allowed any typeclass that had been implemented for TT to be automatically derived for TT'.

GeneralizedNewtypeDeriving was therefore a form of substitution in an arbitrary context, which was in conflict with the equality relation in the rest of Haskell's type system, which considered TT and TT' distinct. In particular, type families are allowed to distinguish TT and TT', leading to this counterexample:

-- Counterexample by Stefan O'Rear
{-# OPTIONS_GHC -ftype-families #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
data family Z :: * -> *

newtype Moo = Moo Int

newtype instance Z Int = ZI Double
newtype instance Z Moo = ZM (Int,Int)

newtype Moo = Moo Int deriving(IsInt)
class IsInt t where
    isInt :: c Int -> c t
instance IsInt Int where isInt = id
main = case isInt (ZI 4.0) of
         ZM tu -> print tu -- segfaults

The fix in Haskell was to introduce roles3, implicitly annotating each type and type parameter according to whether it was used in a context allowing T=TT = T' (the representational role, allowing efficient coercions between newtypes and their underlying types) or an a context assuming TTT \neq T' (the nominal role, used in type families). For more on roles, see the GHC wiki4.


The characterisation of this issue as two conflicting equalities is due to Conor McBride


Safe Zero-cost Coercions for Haskell (ICFP '14), Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, Stephanie Weirich (2014)