On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote:
Alas, g simply discards its argument, so there are no further constraints on 'a'. I think Martin would argue that type inference should succeed with a=Bool, since there is exactly one solution. Is this an example of what you mean?
Actually a = Maybe Bool
However, as a programmer I would not be in the least upset if inference failed, and I was required to add a type signature. I don't expect type inference algorithms to "guess", or to solve recursive equations, and that's what is happening here.
I think Martin is assuming the current Haskell algorithm: infer the type of the function and then check that it's subsumed by the declared type, while you're assuming a bidirectional algorithm. That makes a big difference in this case, but you still do subsumption elsewhere, so Martin's requirement for normal forms will still be present.