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