Rank-2 polymorphism and pattern matching

[Simon Peyton-Jones]

Jim

| My reason for wanting pattern matching on values of polymorphic types
| is a kind of first-level refinement types. I'm going to demonstrate
| using the "risers" function, as presented in Dana N. Xu's ESC/Haskell, which
| references Neil Mitchell's Catch.

I didn't follow all the details, but I think your main idea is to use the fact that [] is the only value of type (forall a. [a]), and similarly for other polymorphic values, and use that to reason that certain branches are inaccessible.

Sadly, it's not true in Haskell, is it?
        (error "urk") : []
also has type (forall a. [a]).

I don't know how to fix this, short of making the constructors strict.

Another less-than-satisfying aspect is that Nil has a real value argument (usually () I guess) which is there only to speak to the type system.  It's nicer if static properties have static witnesses, and involve no runtime activity.

You have a type (NonEmpty (NonEmpty a)). If you expand that out, I think you get a
        forall n1. List (forall n2. List a n2) n1
So you're instantiating the element type of the outer list with a polytype, which requires impredicativity too, not just existentials!

All that said, I never thought of using existentials this way. Ingenious.

Simon