Ross Paterson writes:
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.
A quick reply: Subsumption among two type schemes boilds down to testing whether (roughly) Annotation_Constraint implies Infered_Constraint ^^^^ ^^^^ given demanded iff Annotation_Constraint <-> Annotation_Constraint /\ Infered_Constraint So, of course the latter is more suitable for testing than the former. (effectively, we push 'given' type information down the abstract syntax tree). In any case, it's entirly unclear to me whether 'stopping' the AT inference process at some stage will guarantee complete inference (in the presence of type annotations etc). Martin