fix: non-llambda solutions had incorrect lambda prefix

Possible fix for #155. More testing needed.

CHANGES.md

@@ -10,6 +10,8 @@ Changes
 
 Bugfixes
 
+* Incorrect lambda-prefix for non-Llambda unification problems  
+  (#155, report + fix by @wikku)
 * `Import ... with` now requires the replacements for the declared
   predicates in the importee to be pairwise distinct.  
   (#152, discovered in discussions with Farah Al Wardani @innofarah and Dale

src/unify.ml

@@ -376,12 +376,12 @@ let rec prune_same_var l1 l2 j bl = match l1,l2 with
 
 (* Given a variable [v1] which has access to the terms [a11 ... a1n] via
  * de Bruijn indices,
- *   [make_non_llambda_subst v1 a1 t2]
+ *   [make_non_llambda_subst lev v1 a1 t2]
  * returns a substitution for [v1] which unifies it with [t2]. Here it is
  * assumed that [a1] satisfies the LLambda restriction, but [t2] might not. If
  * a substitution cannot be found due to non-LLambda issues, an error exception
  * is thrown. *)
-let make_non_llambda_subst v1 a1 t2 =
+let make_non_llambda_subst lev v1 a1 t2 =
   let a1 = List.map hnorm a1 in
   let n = List.length a1 in
   let rec aux lev t =
@@ -409,7 +409,7 @@ let make_non_llambda_subst v1 a1 t2 =
           lambda idtys2 (aux (lev + List.length idtys2) b2)
       | _ -> raise (UnifyError NotLLambda)
   in
-    aux 0 t2
+  aux lev t2
 
 (* Here we assume v1 is a variable we want to bind to t2. We must check that
  * there is no-cyclic substitution and that nothing with a timestamp higher
@@ -564,7 +564,7 @@ let makesubst tyctx h1 t2 a1 n =
                         else
                           app h2 a1'
                   else
-                    make_non_llambda_subst hv1 a1 c
+                    make_non_llambda_subst lev hv1 a1 c
             | Var _ -> bugf "logic variable on the left (1)"
             | _ -> assert false
           end
@@ -620,7 +620,7 @@ let makesubst tyctx h1 t2 a1 n =
                       else
                         assert false (* fail TypesMismatch *)
                   else
-                    make_non_llambda_subst hv1 a1 t2
+                    make_non_llambda_subst lev hv1 a1 t2
             | App _ | Lam _
             | Var _ | DB _ ->
                 nested_subst tyctx t2 lev