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) < (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