Type inference systems for functional languages are usually based on Hindley-Milner. Unfortunately, polymorphism in Hindley-Milner is restricted to let-bound values only which restricts expressiveness. An long standing research challenge is to do type inference for full System-F where polymorphism is first-class and where polymorphic values can be passed as arguments or be part of data structures. Since type inference for System-F is undecidable in general, the question is how to use the minimal