let rec unify node1 node2 =
    if not (equivalent node1 node2) then
      match normalize node1, normalize node2, node1, node2 with
      | Variable forbidden1, _, node1, node2
      |        _, Variable forbidden1, node2, node1 ->
          impose forbidden1 node2;
          check node1 node2;
          union node1 node2
      | Constant s1, Constant s2, _, _ ->
          if not (Set.equal s1 s2) then
            raise Error;
          union node1 node2
      | Constant s1, DisjointSum (s2, tail2), node1, node2
      |        DisjointSum (s2, tail2), Constant s1, node2, node1 ->
          if not (subset s2 s1) then
            raise Error;
          unify tail2 (constant (Set.diff s1 s2));
          union node2 node1
      | DisjointSum (s1, tail1), DisjointSum (s2, tail2), _, _ ->
          let s1 = Set.diff s1 s2
          and s2 = Set.diff s2 s1 in
          begin
            match Set.is_empty s1, Set.is_empty s2 with
            | true, true ->
                unify tail1 tail2
            | false, true ->
                unify (_sum s1 tail1) tail2
            | true, false ->
                unify tail1 (_sum s2 tail2)
            | false, false ->
                let tail = variable (Set.union s1 s2) in
                unify tail1 (_sum s2 tail);
                unify tail2 (_sum s1 tail)
          end;
          union node1 node2