18+ kosmikus, 1 month ago @BoydStephenSmithJr I voted RankNTypes. Arguments in favour: RankNTypes (or at least Rank2Types) existed long before GADTs, and RankNTypes can be translated into "plain" Fω Core, without needing any equality constraints like FC.
@BoydStephenSmithJr I voted RankNTypes. Arguments in favour: RankNTypes (or at least Rank2Types) existed long before GADTs, and RankNTypes can be translated into "plain" Fω Core, without needing any equality constraints like FC.