No deref on HO variable when unifying?

[FissoreD]

This code does not work:

type f any -> o.

main :-
  P = x\x,             % p1
  pi x\ f x = A (P x), % p2
  A = f.               % p3

Error msg: Anomaly: Non deterministic pruning, delay to be implemented: t=A1 (≪.X0≫_0 c1), delta=0
I would expect that after p1, p2 becomes pi x\ f x = A x, so that A := (x\ f x) or better A := f

[gares]

Surely a bug

[gares]

Not a bug, but a missing feature. It seems move needs to do no restriction, but instead checks if doing it would be deterministic, and it would be not (but is also unnecessary)

[nguermond]

I want to submit a further example where this would be useful, and not involving a beta reduction:

type subst any -> any -> o.
subst X TX :- T X = TX.       %% X is not dereferenced

main :- pi x \ subst x (foo x).

with the slightly different Unification problem outside the pattern fragment. error.
At runtime, X is an eigenvariable, so it should fall within the pattern fragment.

The more general use case is the following. Given a ground term TX possibly depending on a known list of eigenvariables [x1, ... , xn], it would be useful to solve TX = T x1 ... xn which is in the pattern fragment.

[gares]

This one is not a bug, since T sees X twice (one copy is passed, but T is also generated under the pi...).
This one works as you expected:

type foo any -> any.

type subst (any -> any) -> any -> any -> o.
subst T X TX :- T X = TX.       %% X is not dereferenced

main :- pi x \ subst T x (foo x).

[nguermond]

This makes sense, thanks for catching that.