The example is $(λx.λy.y), where $ is generalization performed by binding to a fresh variable that then gets frozen. In the PLDI paper we give type ∀ab. a → b → b but Frozen Inferno finds ∀b. ∀a. a → b → b. Additional ∀ is not a problem, but reversing the order of quantifiers is. I think this should be addressed once #38 is resolved.
The example is
$(λx.λy.y), where$is generalization performed by binding to a fresh variable that then gets frozen. In the PLDI paper we give type∀ab. a → b → bbut Frozen Inferno finds∀b. ∀a. a → b → b. Additional∀is not a problem, but reversing the order of quantifiers is. I think this should be addressed once #38 is resolved.