Added a test and fixed two inference bugs

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,w)),
-      Exist(tau,Some (Arrow(a,b)),
         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 ->

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

tests.t/trifun.test

@@ -0,0 +1 @@
+lambda f. lambda x. lambda y. f x y