jstolarek / inferno

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

Incorrect ranks of type constructors created from annotations #22

Closed jstolarek closed 3 years ago

jstolarek commented 3 years ago

Consider these two definitions:

let (z : ∀ b. b → Int) =  λw. 1 in
let z' =  λw. 1 in ...

z and z' have the same type but internally their representation is different. Concretely, rank of Int type is set incorrectly to -1 in z:

z  : forall [{id=10, rank=-1}]. {id=12, structure=({id=10, rank=-1} -> {id=11, structure=Int, rank=-1}), rank=-1}
z' : forall [{id=13, rank=-1}]. {id=12, structure=({id=13, rank=-1} -> {id=14, structure=Int, rank=1}), rank=-1}

This breaks mixed_prefix_2 example by allowing a negative-rank variable into the pool. Rewriting that example without a signature on z works correctly (mixed_prefix_2_no_sig). This is a bug with fresh variable generation when converting a type annotation to internal representation.