Skip to content

Fix variables typing

koizel requested to merge fix-variables into devel

Fix typing of the following term

(Set :*) (El (-> Set *)) |- (=> (s Set) (x (El s)) (P (-> (El s) (El s))) (P x))

Before the pull request, that would be transformed into the following nameless representation

... |- (=> Set (El s) (-> (El 1) (El 1)) (0 1))

and typing this term would yield into the following typing tree

 ... |- 0 : (-> (El 1) (El 1))       ... |- 1 : El 0
------------------------------------------------------
 ..., Set, El 0, (-> (El 1) (El 1)) |- (0 1) : (El 2)

but El 1 == El 0 doesn't hold.

The solution is to shift the inferred type of the variable 1 by 1 + <index of var>, hence in that case, 1 + 1, which yields ... |- 1 : el 2 and ... 0 |- : (-> (El 2) (El 2)).

Merge request reports