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


Reply via email to