There's a common pattern in Haskell of writing: data E where E :: C a => a -> E also written data E = forall a. C a => E a I recently uploaded a package to Hackage which uses the new ConstraintKinds extension to factor this pattern out into an Exists type parameterized on the constraint, and also for an Existential type class which can encompass these kind of types: http://hackage.haskell.org/package/exists My motivation was mostly to play with my new toys, if it turns out to be useful for anything that's a happy and unexpected bonus. Some interesting things I stumbled upon while writing it: - Did you know you can write useful existentials for Functor, Foldable, and Traversable? I sure didn't beforehand. - You can even write them for various Comonad classes, though in their case I don't think it's good for anything because you have no way to run them. - Surprisingly to me, the only * kinded class in the standardish libraries I found which is useful with existentials is Show, the * -> * kinded ones are more numerous. - I don't know if anyone's ever set out what the precise requirements are for a type class method to be useful with existentials. For example, any method which requires two arguments of the same type (the type in the class head) is clearly useless, because if you have two existentials there's no way to tell whether or not their contents were of the same type. I think this holds any time you have more than one value of the type among the method's parameters in any kind of way (even if it's e.g. a single parameter that's a list). If the type-from-the-class-head (is there a word for this?) is used in the method's parameters in a position where it's not the outermost type constructor of a type (i.e. it's a type argument), that's also no good, because there's no way to extract the type from the existential, you can only extract the value. On the other hand, in the method's return type it's fine if there are multiple values of the type-from-the-class-head (or if it's used as a type argument?), because (as long as the method also has an argument of the type) the type to put into the resulting existentials can be deduced to be the same as the one that was in the argument. But if the type-from-the-class-head is used *only* in the return type, then it's difficult to construct an existential out of the return value because the instance to use will be ambiguous. - There are a lot of ways you can write existentials, and the library only captures a small part of them. Multiparameter constraint? No go. More than one constraint? No go (though you can use Control.Constraint.Combine). More than one type/value stored? No go. Anything which doesn't exactly match the patterns data E where E :: C a => a -> E or data E a where E :: C f => f a -> E a? No go. I don't think there's any way to capture all of the possibilities in a finite amount of code. - ConstraintKinds lets you write class aliases as type synonyms, type Stringy a = (Show a, Eq a). The old way to do this is class (Show a, Eq a) => Stringy a; instance (Show a, Eq a) => Stringy a and requires UndecidableInstances. But if the alias has multiple parameters, the old way is still superior, because it can be partially applied where type synonyms can't. This is analogous to the situation with type synonyms versus newtype/data declarations, but interestingly, unlike data and newtypes, the class+instance method doesn't require you to do any manual wrapping and unwrapping, only the declaration itself is different. - One of the advantages FunctionalDependencies has over TypeFamilies is that type signatures using them tend to be more readable and concise than ones which have to write out explicit equality constraints. For example, foo :: MonadState s m => s -> m () is nicer than foo :: (MonadState m, State m ~ s) => s -> m (). But with equality superclass constraints (as of GHC 7.2), it's possible to translate from TF-form to FD-form (but not the reverse, as far as I know): class (MonadStateTF m, s ~ State m) => MonadStateFDish s m; instance (MonadStateTF m, s ~ State m) => MonadStateFDish s m. - PolyKinds only seems to be useful as long as there's no value-level representation of the polykinded type involved (it's only used as a phantom). As soon as you have to write 'a' for kind * and 'f a' for kind * -> *, you have to do the duplication manually. Is this right? - Writing this library really made me want to have a type-level "Ord instance" for constraints, more precisely a type-level is-implied-by operator. The typechecker clearly knows that Eq is-implied-by Ord, for example, and that Foo is-implied-by (Foo :&: Bar), but I have no way to ask it, I can only use (~). I tried implementing this with OverlappingInstances, but it seems to be fundamentally impossible because you really need a transitive case (instance (c :<=: d, d :<=: e) => c :<=: e) but the transitive case can't work. (My best understanding is that it's because the typechecker doesn't work forward, seeing "ah, c :<=: d and d :<=: e, therefore c :<=: e"; rather it works backwards, and sees that "c might be :<=: e, if there's a suitable d", but then it has no idea what to choose for d and goes into a loop.) Filing a feature request is in the plans. Er... </ul>. Cheers, ~g