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