termination for FDs and ATs

[Martin Sulzmann]

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