search

jstolarek / inferno

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

Freezing of variables without quantifiers is broken #30

Open jstolarek opened 3 years ago

jstolarek commented 3 years ago

Following recent discussions about isMonoInst predicate I've been investigating examples bad3 and bad4. These examples should fail due to monomorphic instantiation constraint on non-GVal let-bound terms. But these examples have been failing even when this constraint was not implemented. It seems like the problem comes from a bug in freezing that leads to inserting bogus forall quantifiers:

Freezing variable f : {id=4, rank=1}.
 Trying to unifying variables:
  {id=38, structure=forall []. {id=4, rank=1}, rank=1}
  {id=20, structure=forall [{id=18, rank=-1}]. {id=19, structure=({id=18, rank=-1} -> {id=18, rank=-1}), rank=-1}, rank=1}

Freezing f results in forall []. {id=4, rank=1}, which in turn does not unify with forall [{id=18, rank=-1}]. .... This is wrong.

jstolarek commented 3 years ago

Fixed. bad3 is now rejected only if we apply the monomorphic instantiation constraint. Without that constraint it is incorrectly accepted.

jstolarek commented 3 years ago

I am reopening this as a reminder to test freezing of types without quantifiers a bit more once #35 has been properly implemented. We need to make sure that freezing works correctly for unquantified types coming from monomorphising lets.