| it works as expected. which is why I think that the type should be: | | f :: forall t. ((forall b. C t b) => t -> t) | | or, bringing the quantifiers to the front: | | f :: forall t. exists b. (C t b => t -> t) My brain is too small to figure out the consequences of adding first-class existentials to Haskell; nor of how to decide when to universally quantify and when to existentially quantify; nor of what to do when calling a function like f. Oleg's recent message gives many other examples you might like to consider. http://www.haskell.org/pipermail/haskell-cafe/2006-December/020538.html | >Why not reject it right away as ambiguous? | | I thought the reason for that was simply that there are situations in | which f can actually | be called, and op be used, such as "f (0::Int)" with "instance C Int | b"? yes, that's right. Simon