[Haskell-cafe] is Haskell missing a non-instantiating polymorphic case?

[Max Bolingbroke]

On 23 October 2011 06:48, Adam Megacz <megacz at cs.berkeley.edu> wrote:
> The title might be a bit more provocative than necessary.
>
> I'm starting to suspect that there are very useful aspects of the
> parametricity of System F(C) which can't be taken advantage of by Haskell in
> its current state.  To put it briefly, case-matching on a value of type
> (forall n . T n) forces one to instantiate the "n", even though the branch
> taken within the case cannot depend on "n" (parametricity).

I wonder if you can write eta-expansion for a product type containing
an existential given your extension? If I have:

data Id a = Id a

I can currently write:

eta x = Id (case x of Id x -> x)

And I have that eta x != _|_ for all x. But if I have:

data Exists = forall a. Exists a

Then I can't write the equivalent eta-expansion:

eta x = Exists (case x of Exists x -> x)

The closest I can get is:

eta x = Exists (case x of Exists x -> unsafeCoerce x :: ())

I'm not sure if you can do this with your extension but it smells plausible.

Max