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

[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 came up with the simplest example I could and posted it to 
StackOverflow, but there haven't been any successes (despite some 
excellent attempts!):

  http://stackoverflow.com/questions/7720108/

This might sound like an obscure problem, but it actually starts to get 
in the way of the very useful Washburn+Weirich "Boxes Go Bananas" and 
related PHOAS representation.  I've written up a short example of the 
problems that happen here:



The link above also includes a very rough sketch of a proposal for a 
"pcase" construct that doesn't instantiate its argument.

Is it possible to do what I'm attempting without adding "pcase" to the 
language?  Would "pcase" break the soundness of the type system (I 
don't think so) or complicate type inference (probably)?

I'd be interested in any comments/thoughts/help people can offer.

Thanks!

  - a

PS, I suspect that this is somehow related to the issue that Guillemette and
    Monnier mention in section 5.1 of their paper on type-preserving closure
    conversion, although I wasn't able to find the code online in order to be
    sure.