[TYPES] System F type inference

[Michael Hicks]

Hi.

I'm trying to better understand the difficulty with System F type 
inference.  I realize that in general Wells has shown System F 
typability is undecidable due to the undecidability of 
semi-unification.  However, I have yet to arrive at an intuition as to 
the sort of programs that are problematic.  Wells' reduction is from 
semi-unification to System F, but I'd like to better understand the 
reverse: how would a System F inference problem translate to an 
undecidable semi-unification problem?  Henglein presented a 
semi-unification algorithm that seems to work in "natural" cases of 
type inference for ML with polymorphic recursion, so I'm wondering when 
(or whether) this algorithm would be sufficient for System F terms.

If anyone could provide pointers to work on topics related to these 
questions, I'd be grateful (I can post a summary of responses back to 
the list).

Cheers,
Mike