`let` signatures without quantifiers broken when type scheme inferred

[jstolarek]

This is a follow-up on https://github.com/jstolarek/inferno/issues/6#issuecomment-721064026 and https://github.com/jstolarek/inferno/issues/2#issuecomment-719644639, which both point to the same problem. When a signature on a let binding has no quantifiers but the type inferred for the bound term is polymorphic, ranks in the resulting type are incorrect. Here's a minimal example (this is test fml_inst_sig_1):

let id_int : Int → Int = λx.x in id_int 1

Annotation has structure:

{id=6, structure=({id=2, structure=Int, rank=-2} -> {id=1, structure=Int, rank=-2}), rank=-2}

and the inferred type for λx.x is:

{id=7, structure=({id=8, rank=-1} -> {id=8, rank=-1}), rank=-1}

Unifying these types results in type:

{id=6, structure=({id=1, structure=Int, rank=-1} -> {id=1, structure=Int, rank=-1}), rank=-1}

which is incorrect, since variables 6 and 1 have rank -1, which means a quantifier. But there are no quantifiers in this type and the ranks are incorrect. Note that this problem is masked when we instantiate such a type. Despite lack of quantifiers variables with rank -1 are still instantiated to a positive rank because at the moment all variables with rank -1 are instantiated. See #7.

I think the next steps are to fix the following problems:

• [x] write an assertion that catches these incorrect types to ensure that example fml_inst_sig_1 fails
• [x] remove the signature hack
• [x] fix instantiation of nested quantifiers - I should have a test that exposes the problem

and only proceed with fixing this problem once the above are fixed.

[jstolarek]

Assertion added in a252362.

[jstolarek]

Signature hack removed in e2c08b7 - see https://github.com/jstolarek/inferno/issues/2#issuecomment-721245690.

[jstolarek]

Nested quantifier instantiation fixed in f618d20bd8d2496c304c9030531493d3ac9c8644.

[jstolarek]

I'm reopening this just to be able to close it with a proper comment. My earlier solution to this would set a positive rank of the unbound generic variables in an inferred type without quantifiers. This resulted in assigning unbound generic variables to a particular existential without inserting these variables into the pool. This rightly resulted in assertion failure. There are two solutions and both seem to work:

1. Correctly register these variables into the pool when setting their rank
2. Don't bind the unbound generic variables. Instead, make sure that these variables are correctly removed from the pool.

I think the first solution is a correct one: there is no point in creating a copy of an unquantified type at every use site. Moreover, the way pool is currently implemented (mutable array of lists) makes it difficult to remove arbitrary variables from it - this results in cubic complexity - which is a problem for implementing second solution. For this reason I opted for the first solution.