# There's only one Leibniz

Leibniz's characterisation of what it means for $A$ to equal $B$ is
that if $P(A)$ holds for any property

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 $A \sim B$ we can substitute the second occurrence of $A$ for $B$ in $A \simeq A$, so necessarily $A \simeq B$ too.

Haskell^{1} had a soundness issue that arose from trying to have
two distinct equality-like relations^{2}. Haskell supports
`newtype`

, a mechanism for creating a new copy $T'$ of a
previously-defined type $T$, and the `GeneralizedNewtypeDeriving`

mechanism allowed any typeclass that had been implemented for $T$ to be
automatically derived for $T'$.

`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 $T$ and $T'$
distinct. In particular, type families are allowed to distinguish $T$
and $T'$, 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 *roles*^{3}, implicitly
annotating each type and type parameter according to whether it was
used in a context allowing $T = T'$ (the *representational role*,
allowing efficient coercions between newtypes and their underlying
types) or an a context assuming $T \neq T'$ (the *nominal role*, used
in type families). For more on roles, see the GHC wiki^{4}.

^{1}

^{2}

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

^{3}

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