Tallying: failure in recursive calls inside merge make the whole merge fail
Currently Type_tallying.merge
raises an exception if a constraint set is unsolvable. This exception is handled by Type_tallying.type_tallying
but not by merge
itself. Thus, if a recursive call inside merge
fails, the whole call fails.
In particular, tallying fails on the constraint set
'a <= 'b -> 'c
1 <= 'b
'a -> 'c <= ('f -> 'f) -> 'e
(which admits a solution 'a := (1 -> 1), other variables := 1).
Test with
debug tallying [] ( 'a , ( 1 , ('a -> 'c) ) ) ( ('b -> 'c), ( 'b , (('f -> 'f) -> 1) ) );;
(here tallying finds only the solution 'a := Empty
and not the other one).
Normalization generates two constraints, one for 'a := Empty
, the other
{ 'f -> 'f <= 'a <= 'b -> 'c, 1 <= 'b <= Any, Empty <= 'c <= 1 }
which is not solved correctly. In merge
, the contraint
'f -> 'f <= 'b -> 'c
is generated and normalised into
{ { Empty <= 'b <= 'f, 'f <= 'c <= Any }, { Empty <= 'b <= Empty } }
only the first of which is solvable (since 1 <= 'b
, 'b <= Empty
is impossible). The case 'b <= Empty
is considered first and merge
fails completely instead of considering the other case.
Replacing line 605
let m1' = merge delta cache m1 in
with
let m1' = try merge delta cache m1 with UnSatConstr _ -> ConstrSet.unsat in
solves this. I'm not sure if it breaks anything else, but it seems to be what the specification of tallying says (the recursive calls are in union with each other, so empty sets are ignored).