[unification] fix regression #135 (#137)

* [unification] fix regression (fix #135, fix #136)

CHANGES.md

@@ -1,3 +1,8 @@
+# v1.14.1 (February 2022)
+
+- Runtime:
+  - Fix unification dealing with a deep `AppArg` (regression in 1.14.0)
+
 # v1.14.0 (February 2022)
 
 - Runtime/FFI:

src/runtime.ml

@@ -1649,7 +1649,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
          the clause is at 0 and we are under a pi x\. As a result we do the
          deref to and the rec call at adepth *)
       let args =
-        List.map (move ~argsdepth ~from:bdepth ~to_:(adepth+depth) e) args in
+        List.map (move ~argsdepth ~from:bdepth ~to_:adepth e) args in
       unif argsdepth matching depth adepth a adepth
         (deref_appuv ~from:argsdepth ~to_:(adepth+depth) args e.(i)) empty_env
 

tests/sources/eta.elpi

@@ -6,6 +6,11 @@ macro @ctx A :- c (_\ A). % to have depth > 0 in unif
 k1 (x\ g x).
 k2 g.
 
+%mode (foo i i).
+pred foo i:(X -> X), i:(X -> X -> X).
+foo X (x1 \ (x2 \ X x2)) :- (print X).
+%% Fails, but should output `y`
+
 main :-
   pi f y\
     % 4 branches in unif
@@ -20,5 +25,8 @@ main :-
 
     % index + adepth=2 <> bdepth=0
     k1 g,
-    k2 (x\ g x)
+    k2 (x\ g x),
+
+    % regression #135
+    foo y (x1 \ (x2 \ y x2))
 .

tests/sources/hdclause.elpi

@@ -0,0 +1,16 @@
+kind foo type.
+
+type a ((int -> foo) -> foo) -> foo.
+type b foo -> foo.
+
+type p (foo -> foo) -> foo -> prop.
+type q (foo -> foo) -> foo -> prop.
+
+p K (a f\ K (f 0)).
+q K R :- R = (a f\ K (f 0)).
+
+main :-
+  (pi y\ p b (F y)),
+  (pi y\ q b (F y)),
+  (pi x y\ q b (F y)),
+  (pi x y\ p b (F y)).

tests/suite/correctness_HO.ml

@@ -235,3 +235,10 @@ let () = declare "eta_as"
   ~description:"eta expansion of as clause"
   ~typecheck:false
   ()
+
+let () = declare "hdclause"
+  ~source_elpi:"hdclause.elpi"
+  ~description:"hdclause unification"
+  ~typecheck:false
+  ()
+