[Note to the Haskell list. The question this thread is discussing is whether the H98 rule that all the functions in a mutually recursive group must have the same context, is a show stopper.] | Oeer. Come to think of it, if f is getting the dictionary | (in the real world | example) from the context, rather than from the existential | type, I fear it may be getting the wrong dictionary, and will | crash badly when I try to run the code. No I don't think that can happen. But I have thought of a test case data T = forall a. Eq a => MkT a a T | Nil f :: T -> Bool f Nil = True f (MkT x y t) = g x y t g :: Eq b => b -> b -> T -> Bool g x y t = (x==y) && f t Notice that (a) f and g are mutually recursive (b) They have different contexts in their type sig (c) If they were made the same, f would get an ambiguous type f :: Eq a => T -> Bool (d) Haskell's polymorphic recursion is essential here; each call to g may be at a different type So it looks to me that, in the presence of existentials, the H98 rule goes from being moot to being throughly awkward. Mark's THIH paper shows that there's no real need for the rule, because one can type-check the bindings without type sigs as a group, and then the ones with type sigs one by one. But what happens for pattern-bindings that bind more than one variable. Must all those variables have the same context? (I hope so.) Needless to say, I'm not proposing any changes in H98! But I thought the example would be of interest. Maybe it's well known, but it wasn't to me. Simon