Skip to content

Tentative fix for the soundness bug in the subtyping algorithm.

Kim Nguyễn requested to merge subtyping-debug into dev

Tentative fix for Issue #37 (closed). Witnesses used to check the non-emptyness of a type are extended with "polymorphic witnesses".

A polymorphic witness is a triple of a set of positive variable, a set of negative variables and a plain (monomorphic witness).

Recall that a witness for Any is e.g. 0 (that is, since Any = Int | Char | ... , then when a witness for Any is needed, an inhabitant of Int is choosen first and in particular 0).

We used to also return 0 for the type 'a (by wrongly applying the algorithm of the ICFP'11 Paper which discards toplevel variables). Here, we return a witness ('a&0). Now, when we check, e.g. if 'a&0 belongs to Int'a, we answer no (while previously we would answer that 0 belongs to Int).

This seems to fix the problem. This commit also adds a file to host new tests specifically for subtyping.

Merge request reports