Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism (Artifact)

This project implements the algorithmic type system presented in the paper "Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism", which supports strong existential types, higher-rank polymorphism, and polymorphic subtyping. Most importantly, we support existential quantification and existential projections (as defined in the paper). This tool is built upon the implementation for Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.