Indeed! Empty is lucky. The existence, for a type x, of a function

impossible :: forall y . x -> y

is sufficient--parametricity guarantees uniqueness. For Boring/Singular, this is certainly not the case. Non-boring types y typically have multiple functions

possible :: forall x . x -> y

We'd really want

sole :: Pi (y :: a) -> inhabitant = y

For some horrifyingly vague notion of equality. That obviously isn't going to cut it for real Haskell.