Tallying: monomorphic variables are not handled correctly
When we perform tallying with a non-empty delta and types contain top-level variables that are in delta, we do not handle them correctly.
See
debug tallying ['b] [ ('a, Int) , 'b ];;
(no solution found, while 'a<-Empty
works) and
debug tallying ['b] [ ('a, Int) , 'b | 'c ];;
(no solution found, while it works if we use ['c]
as delta instead).
The problem is in Type_tallying.toplevel (line 245). We can probably fix it as follows. Currently, we always pick the first variable (positive or negative) that we find (we give priority to polymorphic ones only in one branch of matching). Instead, as long as there is at least one polymorphic variable, we should prefer it to monomorphic ones.
If all variables are monomorphic, we should basically test for emptiness of the type without these monomorphic variables. Say the smallest variable is 'a
and is positive; thus we have t & 'a
. For emptiness we need t <: not('a)
. However, this should be possible only if t
contains not('a)
(which maybe never happens because we would have simplified the type?) or if it is empty (which we surely need to check).