Rank-2 polymorphism and pattern matching

[Jim Apple]

On Jan 7, 2008 1:37 AM, Simon Peyton-Jones <simonpj at microsoft.com> wrote:
> Sadly, it's not true in Haskell, is it?
>         (error "urk") : []
> also has type (forall a. [a]).

It is a bit sad, but I think that's The Curse of The _|_, which
infects any attempt to add static assurance.

> It's nicer if static properties have static witnesses, and involve no runtime activity.

Maybe The Curse doesn't infect everything. What methods of assuring
static properties in GHC have static witnesses?

I think no: GADTs, lightweight static capabilities, forall a . [a]
trick, nested/non-regular types
I think yes: associated types, class constraints

> 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!

It's true, but that seems to work without a hiccup right now

Jim