Hello. < class C t where op :: t -> Bool < instance C [t] where op x = True < < p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ []) < q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f) < <The definitions of p and q differ only in the order of the components in <the pair on their right-hand sides. And yet: < < ghc and "Typing Haskell in Haskell" reject p, but accept q; < Hugs rejects q, but accepts p; < hbc rejects both p and q; < nhc98 ... (Malcolm, can you fill in the blank for us!). System CT accepts both. No type signature is required. The types inferred for p and q are, resp.: Forall a,b. [a] -> (b -> Bool, [a]) and Forall a,b. [a] -> ([a], b -> Bool) You can run the attached "encoded" program (in which 'op' is overloaded, instead of having its type annotated in a type class) in CTinH (http://www.dcc.ufmg.br/~camarao/CT/CTinH.tar.gz). Type inference in system CT is explained in a paper available at http://www.dcc.ufmg.br/~camarao/CT/CT.ps.gz (see also homepage at http://www.dcc.ufmg.br/~camarao/CT). Carlos