try_right_unify_cpairs failure

[robblanco]

I have run into and isolated the following issue. My expectation is that Unify.try_right_unify_cpairs should succeed, but it does not. I have run this through @thatdalemiller, and he seems to agree, provided that I did not miss anything important.

The following test on the default signature reproduces the problem. It can be added directly to Test_unify, or taken from branch bug-try_right_unify_cpairs in my local fork.

      "Plus-like decomposition" >::
        (fun () ->
           let str = "exists X Y Z,\
(iapp (r1 t1) (iapp (r1 (r1 t1)) (iapp (r1 (r1 (r1 t1))) t2))) =\
(iapp (r1 X ) (iapp Y            (iapp (r1 Z           ) t2)))" in
           match parse_metaterm str with
             | Binding(Exists, _, (Eq(left, right))) ->
                 begin match try_right_unify_cpairs left right with
                   | None ->
                       assert_failure "Unification expected to succeed"
                   | _ -> ()
                 end
             | _ -> assert false
        );

[chaudhuri]

Unless you substitute logic variables for X, Y, and Z, they will have tag Constant, which means that they are not instantiable on the right. You can see this by uncommenting show_tag in term.ml, which will show you the tags on all variables.

[chaudhuri]

I mean setting show_tag to true.

[robblanco]

In the runtime equivalent of the test (in the context of my program) they are proper logic variables, or I have interpreted them to be, i.e., they will be prettyprinted as ?1, ?2, etc. I will take another look.

[robblanco]

Indeed, the analogs in my program are logic variables. The test doesn't reflect this, so I will change it and see what happens. I'm still pretty sure the error is there.

[robblanco]

I tracked down the error down to my local flavor of the search tactic, thanks to your debugging tip. I have found inspecting variables programmatically rather inconvenient, and that helped narrow down an incorrect assumption. I think at least some variable attributes should be readable, but that's a discussion for another day. I'm closing the issue now.