If I have a function: f x y = add x y and I want to type the function in isolation, then the type of 'add' is essentially carried in the environment... Lets say I want to make this type explicit in the type signature (where f is valid for any a where there is an add function on a - ignoring the class that Haskell would require for the overloading): add :: Int -> Int -> Int add :: Float -> Float -> Float f :: forall a . exists (add :: a -> a -> a) => a -> a -> a or a step further: class Add a where add :: a -> a -> a instance Add Int where ... instance Add Float where ... f :: forall a . Add a => a -> a -> a This seems to suggest: Add a == exists (add :: a -> a -> a) Does this seem in any way right? It seems that the definition of 'f' does require the existance of 'add'. That is the definition is valid iff there exists a function called 'add' of the correct type. Also doesn't the existential quantifier stop you looking inside 'add' - obviously you cannot inspect the definition as it may not be defined (yet?), but presumably you can still apply 'add'. Regards, Keean.