Let me see if I have the implementation correct. To typecheck f :: signature f = ... f ... you would first set the type of f from the signature, typecheck the body of f, and then ensure that the inferred type agrees with the signature. This sounds quite reasonable to me. I suppose the hardest bit is explaining to the user why the type signature may be required to allow type checking, but as has been said before we have already done this for monomorphism (not that many Haskell users really understand the monomorphism restriction!!). I suppose you could extend this to provide polymorphic function parameters: f :: (a -> a) -> b -> c -> (b,c) f fn x y = (fn x, fn y) but I'm probably getting off the topic here. John
