On 23 October 2011 06:48, Adam Megacz
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