- Using ranked type variables instead of scanning the complete Γ to achieve efficiency.
- Support adding extra type annotations for First-Class Polymorphism, it is indeed decidable and sound.
- Support explicit type annotations for Basic Polymorphism and infer series of terms.