Instantiation of nested quantifier might not work as expected

[jstolarek]

Generalize.instantiate currently instantiates all quantifiers it encounters as part of a variable graph, but it should only instantiate the top-level ones, not the nested ones. I need to write an example yet that will trigger the problem. I've implemented a speculative fixed but it's currently commented out.

[jstolarek]

Ok, here's an example that exposes the problem:

let (f : ∀ a. ((∀ b. b → b) → a → a) → ((∀ b. b → b) → a → a)) = id in
let g = f (id auto') in
g ~id

(I am not 100% sure it is type correct, but for it is causing an assertion failure anyway, which is exactly what it was intended to do.)

Looking at the logs I can see that f has type:

forall [{id=1, rank=-1}]. {id=12, structure=(
  {id=6, structure=({id=5, structure=forall [{id=3, rank=-1}].{ id=4, structure=({id=3, rank=-1} -> {id=3, rank=-1}), rank=-1}, rank=-1} ->
     {id=2, structure=({id=1, rank=-1} -> {id=1, rank=-1}), rank=-1}), rank=-1} ->
  {id=6, structure=({id=5, structure=forall [{id=3, rank=-1}]. {id=4, structure=({id=3, rank=-1} -> {id=3, rank=-1}), rank=-1}, rank=-1} ->
     {id=2, structure=({id=1, rank=-1} -> {id=1, rank=-1}), rank=-1}), rank=-1}), rank=-1}.

And that is correct. Then this type gets instantiated to:

{id=43, structure=(
  {id=44, structure=({id=45, structure=forall [{id=46, rank=2}]. {id=47, structure=({id=46, rank=2} -> {id=46, rank=2}), rank=2}, rank=2} ->
     {id=48, structure=({id=49, rank=2} -> {id=49, rank=2}), rank=2}), rank=2} ->
  {id=44, structure=({id=45, structure=forall [{id=46, rank=2}]. {id=47, structure=({id=46, rank=2} -> {id=46, rank=2}), rank=2}, rank=2} ->
     {id=48, structure=({id=49, rank=2} -> {id=49, rank=2}), rank=2}), rank=2}), rank=2}

where nested quantifiers are instantiated and receive rank 2 (variables 46 and 47).