termination for FDs and ATs

[Ross Paterson]

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.