<p dir="ltr">The () kind has infinitely many inhabitants: the type '() and any stuck or looping types with appropriate kinds. However, I've not been able to find a way to break type safety with the postulate</p>
<p dir="ltr">unitsEqual :: (a :: ()) :~: (b :: ())</p>
<p dir="ltr">in GHC 7.10.3 (it was possible using a now-rejected data family in 7.8.3). Is there some way I haven't found yet, or is this safe? If it's *not* safe, is the equivalent postulate using Void instead of () safe? For my purposes, () would be nicer, but it feels riskier.</p>