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

I agree that this should be safe, although it would be nice if someone proved it! Another way to think of it is as a consequence of the eta rule: forall (a :: ()) . a ~ '() There is an existing feature request [1] to add eta conversion to GHC, which should include this. All the best, Adam [1] https://ghc.haskell.org/trac/ghc/ticket/7259 On 12/04/16 01:49, Richard Eisenberg wrote:

I believe this is safe, yes.

Saying the kind () has infinitely many types in it is somewhat like saying the type () has infinitely many terms in it, like (), undefined, undefined 1, undefined False, ... With the change to type families in the past few years, it should be impossible to match on any inhabitant of the kind () except the type '(). That makes the postulate you postulate quite sensible.

Richard

On Apr 11, 2016, at 4:07 PM, David Feuer mailto:david.feuer@gmail.com> wrote:

...

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.

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/