There's only one Leibniz

[equality]

Leibniz's characterisation of what it means for $A$ to equal $B$ is that if $P(A)$ holds for any property $P$, then so does $P(B)$. In other words, equality is the relation that allows substitution of $B$ for $A$ 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 $A \sim B$ we can substitute the second occurrence of $A$ for $B$ in $A \simeq A$, so necessarily $A \simeq B$ too.

Haskell¹ had a soundness issue that arose from trying to have two distinct equality-like relations². 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³, 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⁴.