Are you aware that the TAPL book comes with an implementation of System F?

https://www.cis.upenn.edu/~bcpierce/tapl/checkers/fullpoly/