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

@@ -35,17 +35,11 @@ curryType ty = case typeArgs ty of
   [] ->
     ty
   tyargs ->
-    let ty' = curryType (typeTarget ty)
+    foldr (\tyarg ty'' -> mkTypeFun [tyarg] ty'') (curryType (typeTarget ty)) tyargs
-     in foldr (\tyarg ty'' -> mkTypeFun [tyarg] ty'') (typeTarget ty') tyargs
 
 isSubtype :: Type -> Type -> Bool
 isSubtype ty1 ty2 =
-  let (ty1', ty2') =
+  let (ty1', ty2') = (curryType ty1, curryType ty2)
-        if
-            | typeTarget (uncurryType ty1) == TyDynamic || typeTarget (uncurryType ty2) == TyDynamic ->
-                (curryType ty1, curryType ty2)
-            | otherwise ->
-                (ty1, 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') =
+  let (ty1', ty2') = (curryType ty1, curryType ty2)
-        if
-            | typeTarget (uncurryType ty1) == TyDynamic || typeTarget (uncurryType ty2) == TyDynamic ->
-                (curryType ty1, curryType ty2)
-            | otherwise ->
-                (ty1, 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)

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")
   ]

tests/Tree/positive/out/test042.out

@@ -0,0 +1 @@
+true

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