diff --git a/CHANGES.md b/CHANGES.md
index 905749574..54c790653 100644
--- a/CHANGES.md
+++ b/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:
diff --git a/src/runtime.ml b/src/runtime.ml
index f2adceff6..13482f174 100644
--- a/src/runtime.ml
+++ b/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
 
diff --git a/tests/sources/eta.elpi b/tests/sources/eta.elpi
index 913b40be5..f8fe5e047 100644
--- a/tests/sources/eta.elpi
+++ b/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))
 .
diff --git a/tests/sources/hdclause.elpi b/tests/sources/hdclause.elpi
new file mode 100644
index 000000000..e4ab29e08
--- /dev/null
+++ b/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)).
diff --git a/tests/suite/correctness_HO.ml b/tests/suite/correctness_HO.ml
index acb70a293..f25eee22a 100644
--- a/tests/suite/correctness_HO.ml
+++ b/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
+  ()
+  
\ No newline at end of file