On Jan 7, 2008 1:37 AM, Simon Peyton-Jones
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