jstolarek / inferno

Mirrored from https://gitlab.inria.fr/fpottier/inferno
MIT License
0 stars 1 forks source link

Instantiation of nested quantifiers broken #19

Closed jstolarek closed 3 years ago

jstolarek commented 3 years ago

When instantiating scheme ∀ a.a → (∀ b. a → a) → Int occurrences of a nested inside the second type scheme are not instantiated. On 7a57214 running mixed_prefix_2 test with debug output shows:

Instantiating type scheme for x : forall [{id=2, rank=-1}]. {id=7, structure=(
   {id=6, structure=forall [{id=4, rank=-1}].
      {id=5, structure=({id=4, rank=-1} -> {id=2, rank=-1}), rank=-1}, rank=-1} ->
      {id=3, structure=Int, rank=-1}), rank=-1}.
 Trying to unifying variables:
  {id=29, structure=({id=30, structure=forall [{id=4, rank=-1}].
        {id=5, structure=({id=4, rank=-1} -> {id=2, rank=-1}), rank=-1}, rank=1} -> {id=31, structure=Int, rank=1}), rank=1}
  {id=15, structure=({id=14, rank=1} -> {id=0, rank=1}), rank=1}

Variable id=29 is an instantiated copy of x and it is clear that it still contains id=2, which should have been instantiated.