[Haskell-cafe] Is it safe to postulate () has one inhabitant?

[David Feuer]

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

unitsEqual :: (a :: ()) :~: (b :: ())

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160411/28f34130/attachment.html>