From 7760267bcda4f6646c4f388cbbba18505af6b3ae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Wed, 9 Oct 2024 15:33:42 +0200
Subject: [PATCH] Fix JuvixTree unification (#3087)

* Closes #3016
* Fixes the `curryType` function
* Changes the behaviour of `unifyTypes` and `isSubtype` to always curry
first
---
 src/Juvix/Compiler/Tree/Extra/Type.hs | 28 ++++-----------------------
 test/Tree/Eval/Positive.hs            |  7 ++++++-
 tests/Tree/positive/out/test042.out   |  1 +
 tests/Tree/positive/test042.jvt       | 25 ++++++++++++++++++++++++
 4 files changed, 36 insertions(+), 25 deletions(-)
 create mode 100644 tests/Tree/positive/out/test042.out
 create mode 100644 tests/Tree/positive/test042.jvt

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
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)
+  }
+}