There have been some nice papers about simple type inference for System F: "HMF: Simple Type Inference for First-Class Polymorphism", "Practical type inference for arbitrary-rank types", and "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism". These algorithms require varying amounts of annotations from the user in order to do the type inference. I am unable to find any papers on how to do type inference for System F-omega though. My questions:
- Can the above algorithms be extended to handle System F-omega (maybe with some more required annotations)? Or do the type lambdas require a different approach?
- Given that explicitly typed (Church-style) System F-omega is easy to type check, could we use one of the above algorithms to do type inference on the System F subset while requiring explicit types for the type lambdas, or do the type lambdas "infect" the other parts so that we cannot do this.
- Is type inference for System F-omega simpler than type inference for dependent types or do they basically need the same techniques (higher-order unification)?