From 88994419e33ad09d065f0806e30547ca15e9d744 Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Thu, 14 Mar 2024 13:54:36 +0100
Subject: [PATCH] Added a test and fixed two inference bugs

---
 src/Infer.ml        | 9 ++++-----
 src/Structure.ml    | 6 +++++-
 tests.t/trifun.test | 1 +
 3 files changed, 10 insertions(+), 6 deletions(-)
 create mode 100644 tests.t/trifun.test

diff --git a/src/Infer.ml b/src/Infer.ml
index 38d2cbc..7d4254b 100644
--- a/src/Infer.ml
+++ b/src/Infer.ml
@@ -109,14 +109,13 @@ module Make(T : Utils.Functor) = struct
           (Env.find_opt x env)
       )
     | Untyped.App (t, u) ->
-      let a,b,tau = Var.fresh "a", Var.fresh "b", Var.fresh "τ" in
+      let a,tau = Var.fresh "a", Var.fresh "τ" in
       Exist(a,None,
-      Exist(b,None,
-      Exist(tau,Some (Arrow(a,b)),
+      Exist(tau,Some (Arrow(a,w)),
         Map(
           Conj(has_type env t tau,has_type env u a),
           fun (tt,uu) -> App(tt,uu)
-      ))))
+      )))
     | Untyped.Abs (x, t) -> 
         let tau,a,b = Var.fresh "τ",Var.fresh "α", Var.fresh "β" in
         let newenv = Env.add x a env in
@@ -152,7 +151,7 @@ module Make(T : Utils.Functor) = struct
         ))
     | Untyped.Annot (t, ty) ->
         Map(
-          bind ty (fun w -> has_type env t w),
+          bind ty (fun ww -> Map(Conj(eq w ww,has_type env t ww),snd)),
           fun tt -> STLC.Annot(tt,ty)
         )
     | Untyped.Tuple ts ->
diff --git a/src/Structure.ml b/src/Structure.ml
index 0e1793d..351fb40 100644
--- a/src/Structure.ml
+++ b/src/Structure.ml
@@ -46,7 +46,11 @@ let map f = function
   | Prod ts -> Prod (List.map f ts)
 
 let merge f s1 s2 =
-    Utils.not_yet "Structure.merge" (f, s1, s2)
+    match (s1,s2) with
+    | Var(x),Var(y) -> if x=y then Some(Var(x)) else None
+    | Arrow(s,t),Arrow(u,v) -> Some(Arrow(f s u, f t v))
+    | Prod(t),Prod(u) -> Some(Prod(List.map2 f t u))
+    | _ -> None
 
 let global_tyvar : string -> TyVar.t =
   (* There are no binders for type variables, which are scoped
diff --git a/tests.t/trifun.test b/tests.t/trifun.test
new file mode 100644
index 0000000..491380d
--- /dev/null
+++ b/tests.t/trifun.test
@@ -0,0 +1 @@
+lambda f. lambda x. lambda y. f x y