| data Eq a => Set a = Set (List a) | | that is a sort of extension i will be glad to see. in my Streams | library, it's a typical beast and i forced to move all these contexts | to the instances/functions definitions: Another reasonable alternative is data Set a = Eq a => Set (List a) Operationally, a dictionary for (Eq a) is stored in the Set constructor along with the List a. Haskell (and GHC) doesn't allow this at the moment, but it would make perfect sense to do so, I think. The type of Set remains Set :: forall a. Eq a => List a -> Set a The type of member would become member :: a -> Set a -> Bool (with no Eq constraint). The typing rule for 'case' on a constructor with a context, like Set, would be to make the Eq dictionary available in the right-hand side of the case alternative: case e of { Set xs -> ....Eq a available in here... } I am not sure whether it would address all of the cases in John's paper, but it'd address some of them. It would be a significantly less radical step than Restricted Data Types I think. In particular, with GADTs imagine: data T where C :: forall a b. (Eq a, Num b) => a -> a -> b -> T b All Haskell compilers that support existentials will capture the (Eq a) dictionary, and make it available to the rhs of the case alternative. It would be weird not to capture the (Num b) dictionary in the same way. In short, a sensible design for GADTs will pretty much have to embrace this. GHC's implementation is trailing this a bit, I'm afraid, as GADT users will know. Making GADTs and type classes play nicely, particularly with a typed intermediate language, is interesting. Simon