From 3da429d885610e094d8b239bafbc8323b284c8c5 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 7 Oct 2024 18:44:28 +0200
Subject: [PATCH 1/4] merge containers into stdlib

---
 juvix-stdlib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/juvix-stdlib b/juvix-stdlib
index 6010ad32f8..0e143831c4 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 6010ad32f80498432b9a14752a0b7b50e9b36763
+Subproject commit 0e143831c4fcd4dd4cfac6c61907232f10dabcf0

From 331219d26591790eb71a909edd654cf3a5f971f6 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 8 Oct 2024 15:13:24 +0200
Subject: [PATCH 2/4] fix JuvixTree type unification

---
 src/Juvix/Compiler/Tree/Extra/Type.hs | 28 ++++-----------------------
 1 file changed, 4 insertions(+), 24 deletions(-)

diff --git a/src/Juvix/Compiler/Tree/Extra/Type.hs b/src/Juvix/Compiler/Tree/Extra/Type.hs
index a31492c64d..4bf501d624 100644
--- a/src/Juvix/Compiler/Tree/Extra/Type.hs
+++ b/src/Juvix/Compiler/Tree/Extra/Type.hs
@@ -35,17 +35,11 @@ curryType ty = case typeArgs ty of
   [] ->
     ty
   tyargs ->
-    let ty' = curryType (typeTarget ty)
-     in foldr (\tyarg ty'' -> mkTypeFun [tyarg] ty'') (typeTarget ty') tyargs
+    foldr (\tyarg ty'' -> mkTypeFun [tyarg] ty'') (curryType (typeTarget ty)) tyargs
 
 isSubtype :: Type -> Type -> Bool
 isSubtype ty1 ty2 =
-  let (ty1', ty2') =
-        if
-            | typeTarget (uncurryType ty1) == TyDynamic || typeTarget (uncurryType ty2) == TyDynamic ->
-                (curryType ty1, curryType ty2)
-            | otherwise ->
-                (ty1, ty2)
+  let (ty1', ty2') = (curryType ty1, curryType ty2)
    in case (ty1', ty2') of
         (TyDynamic, _) -> True
         (_, TyDynamic) -> True
@@ -96,12 +90,7 @@ isSubtype ty1 ty2 =
 
 unifyTypes :: forall t e r. (Members '[Error TreeError, Reader (Maybe Location), Reader (InfoTable' t e)] r) => Type -> Type -> Sem r Type
 unifyTypes ty1 ty2 =
-  let (ty1', ty2') =
-        if
-            | typeTarget (uncurryType ty1) == TyDynamic || typeTarget (uncurryType ty2) == TyDynamic ->
-                (curryType ty1, curryType ty2)
-            | otherwise ->
-                (ty1, ty2)
+  let (ty1', ty2') = (curryType ty1, curryType ty2)
    in case (ty1', ty2') of
         (TyDynamic, x) -> return x
         (x, TyDynamic) -> return x
@@ -171,13 +160,4 @@ unifyTypes' :: forall t e r. (Member (Error TreeError) r) => Maybe Location -> I
 unifyTypes' loc tab ty1 ty2 =
   runReader loc $
     runReader tab $
-      -- The `if` is to ensure correct behaviour with dynamic type targets. E.g.
-      -- `(A, B) -> *` should unify with `A -> B -> C -> D`.
-      if
-          | tgt1 == TyDynamic || tgt2 == TyDynamic ->
-              unifyTypes @t @e (curryType ty1) (curryType ty2)
-          | otherwise ->
-              unifyTypes @t @e ty1 ty2
-  where
-    tgt1 = typeTarget (uncurryType ty1)
-    tgt2 = typeTarget (uncurryType ty2)
+      unifyTypes @t @e ty1 ty2

From 827c4ed2dfa5772745e60a79c6ecd866d97dbd4d Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 8 Oct 2024 15:17:24 +0200
Subject: [PATCH 3/4] Revert "merge containers into stdlib"

This reverts commit 2c0468127007a652a1f3759466ce76c32ae9fe8f.
---
 juvix-stdlib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/juvix-stdlib b/juvix-stdlib
index 0e143831c4..6010ad32f8 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 0e143831c4fcd4dd4cfac6c61907232f10dabcf0
+Subproject commit 6010ad32f80498432b9a14752a0b7b50e9b36763

From 97a114fae0667dee49f1e6efee5d7742c8ccee47 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 9 Oct 2024 10:54:23 +0200
Subject: [PATCH 4/4] add test

---
 test/Tree/Eval/Positive.hs          |  7 ++++++-
 tests/Tree/positive/out/test042.out |  1 +
 tests/Tree/positive/test042.jvt     | 25 +++++++++++++++++++++++++
 3 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 tests/Tree/positive/out/test042.out
 create mode 100644 tests/Tree/positive/test042.jvt

diff --git a/test/Tree/Eval/Positive.hs b/test/Tree/Eval/Positive.hs
index 3f6ad1aca4..6026e3a577 100644
--- a/test/Tree/Eval/Positive.hs
+++ b/test/Tree/Eval/Positive.hs
@@ -244,5 +244,10 @@ tests =
       "Test041: Type unification"
       $(mkRelDir ".")
       $(mkRelFile "test041.jvt")
-      $(mkRelFile "out/test041.out")
+      $(mkRelFile "out/test041.out"),
+    PosTest
+      "Test042: Uncurried function type unification"
+      $(mkRelDir ".")
+      $(mkRelFile "test042.jvt")
+      $(mkRelFile "out/test042.out")
   ]
diff --git a/tests/Tree/positive/out/test042.out b/tests/Tree/positive/out/test042.out
new file mode 100644
index 0000000000..27ba77ddaf
--- /dev/null
+++ b/tests/Tree/positive/out/test042.out
@@ -0,0 +1 @@
+true
diff --git a/tests/Tree/positive/test042.jvt b/tests/Tree/positive/test042.jvt
new file mode 100644
index 0000000000..d591d9f053
--- /dev/null
+++ b/tests/Tree/positive/test042.jvt
@@ -0,0 +1,25 @@
+type Eq {
+  mkEq : ((*, *) → bool) → Eq;
+}
+
+function lambda_app(f : (*, *) → bool, a : *, b : *) : bool {
+  ccall(f, a, b)
+}
+
+function spec(Eq) : Eq {
+  alloc[mkEq](calloc[lambda_app](case[Eq](arg[0]) {
+    mkEq: save {
+      tmp[0].mkEq[0]
+    }
+  }))
+}
+
+function cmp(integer, integer) : bool {
+  lt(arg[0], arg[1])
+}
+
+function main() : bool {
+  save(call[spec](alloc[mkEq](calloc[cmp]()))) {
+    ccall(tmp[0].mkEq[0], 1, 2)
+  }
+}