Variable confusion/ill typed terms with higher-order terms

[wikku]

Script:

Kind expr type.

Type mu ((expr -> expr) -> expr) -> expr.

Define foo : expr -> expr -> prop by
  foo (mu k\ E k) (mu k_\ E (o\ o)).

Theorem bar : forall E E', nabla (x : expr), foo (E x) (E' x) -> true.
  intros. case H1 (keep).

Output:

Variables: E1
H1 : foo (mu (k\E1 n1 k)) (mu (k_\E1 k_ o\o))
============================
 true

Expected:

Variables: E1
H1 : foo (mu (k\E1 n1 k)) (mu (k_\E1 n1 o\o))
============================
 true

That is, instead of n1 : expr we have k_ : expr -> expr.

The motivation is the third-order representation of λμ-calculus. foo takes a μ-term and performs structural substitution with the empty continuation under the binder, making the continuation variable unused.

[chaudhuri]

Looks like an issue with imitation in the unification engine. Simpler test case:

Set instantiations on.
Set types on.

Kind i type.
Type k i.
Type m (i -> i) -> i.

Theorem bad :
  forall (G : i -> i) (E : i -> i -> i),
  nabla (x : i),
  G x = m u\ E x k ->
  G k = m u\ E k k. /* should be provable but isn't */
intros. case H1.
/*
Variables: 
  E : i -> i -> i
G <-- z1\m (u\E u k)
============================
 m (u\E u k) = m (u\E k k)
*/

This is probably also a soundness bug.

[ThatDaleMiller]

I played with the unification bug a bit, trying to get Abella to use it to prove false. I didn't manage that (yet), but I did get Abella to generate a "naked OCaml exception". Maybe this helps in debugging efforts. I'm using Abella 2.0.8.

Kind i type.
Type k i.
Type m (i -> i) -> i.

Theorem one : forall (G : i -> i) H, (nabla x, (G x) = (H x)) -> G = H.
intros. case H1. search.

Theorem two :
  forall (G : i -> i) (E : i -> i -> i), 
  (nabla (x : i),G x = m u\ E x k) -> G k = m u\ E k k -> false.
intros. apply one to H1. case H1.
 case H3. /* Error: Invalid_argument("List.for_all2") etc. */

[wikku]

The incorrect binding G <-- z1\m (u\E u k) is generated by makesubst for G n1, m (u\E n1 k). ~It appears that a precondition for nested_subst is violated:~ (misunderstood this probably)

https://github.com/abella-prover/abella/blob/783ff606a31576a611f52ce3ba125f9c576dc83d/src/unify.ml#L489C17-L490C31

[chaudhuri]

Yeah, I think that precondition is for the variable being substituted for, not about bound variables.

Anyway, I think I have an idea of what is causing this bug, but I don't yet know how to fix it. The problem comes from lines 395-396 of unify.ml, which is something that was added during the polymorphism branch merge. If those lines are commented, the non-pattern unification problem is left unsolved, which is still not ideal but is at least sound.

[wikku]

Isn't it suspicious that make_non_llambda_subst doesn't get passed a level and starts with level 0? I added a parameter and pass lev in nested_subst and toplevel_subst and it appears to fix this problem. Tests also pass.

[chaudhuri]

Hmm. Interesting. I've just committed your suggestion.

It looks possible as the source of the issue, but this leaves me very puzzled. This is touching some ancient parts of Abella which date back to when Andrew took Gopalan's original unification code from his "Practical Higher-Order Pattern Unification With On-the-Fly Raising" paper. I'll have to do a closer read to see if indeed this was a bug in translating from SML to OCaml or from somewhere else (or indeed if it's the source of the bug at all).

Thanks again!

[chaudhuri]

@gnadathur97 This bug report and discussion may be of interest to you.

[wikku]

Just some notes. Compare the calls (in the broken code) between good and bad cases:

Kind i type.
Type k i.
Type m (i -> i) -> i.

Theorem good : forall (G : i -> i -> i) (E : i -> i -> i), nabla (x : i),
    G x = u\ E x k  ->  G k = u\ E k k.
  intros. case H1.
  /* make_subst  h1=G  t2=E n1 k  a1=[n1 x2]  n=2
     make_non_llambda_subst  v1=G  a1=[n1 x2]  t2=E n1 k  */
  search. /* OK */

Theorem bad : forall (G : i -> i) (E : i -> i -> i), nabla (x : i),
    G x = m u\ E x k  ->  G k = m u\ E k k.
  intros. case H1.
  /* make_subst  h1=G  t2=m (u\E n1 k)  a1=[n1]  n=1
     make_non_llambda_subst  v1=G  a1=[n1]  t2=E n1 k  */

In the good case, we have a toplevel expansion which adds the x2 argument. The calls to make_non_llambda_subst have different arguments a1, but they should return the same thing. An offset in the form of a level seems natural, and I think it makes sense looking at the code.

The rigid_path_check function also seems to start from level 0, but it's only called from the toplevel so it should be ok.

[wikku]

I think I found another weird case (isn't fixed by 38fda7a)

Kind i type.

Theorem bad :
    forall (T : i -> i) (E : (i -> i) -> i -> i) D,
    nabla n1 n2,
    (forall T (E : (i -> i) -> i) (D : i), nabla k x, E k = D -> T x = D -> E T = D)
    -> T n2 = D
    -> E n1 n2 = D
    -> false.
  intros. apply H1 to H3 H2.

results in

H1 : forall T E D, nabla k x, E k = D -> T x = D -> E T = D
H2 : T n2 = D
H3 : E n1 n2 = D
H4 : E (z3\T n2) n2 = D

I'd expect

H4 : E (z3\T z3) n2 = D

[chaudhuri]

This looks fine to me. Your intended full instance is:

apply H1 to H3 H2 with E = k\ E k n2, T = T, k = n1, x = n2

However, the error message makes it clear why this cannot be allowed:

Error: Invalid instantiation x = n2
 n2 already occurs in the support

In effect, when you apply H1 to _ H2, you enlarge the support of H1 to include n2, and hence the nabla x in H1 now quantifies over something other than n2. Thus, the instance T = T is invalid.

[chaudhuri]

Closing as fixed for now. If you find anything else, please comment and I'll reopen. Thanks again.