GitLab

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).