fix unification

nice commit message

Author: plt-amy

amuletml.cabal

@@ -1,5 +1,5 @@
 name:                amuletml
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:            A functional programming language
 homepage:            https://amulet.ml
 license:             BSD3

src/Types/Unify.hs

@@ -655,15 +655,27 @@ unify scope (TyOperator l v r) (TyOperator l' v' r')
 
 unify scope ta@(TyApps (TyCon v) xs@(_:_)) b = do
   x <- view solveInfo
+  traceM (show (x ^. at v))
   case x ^. at v of
     Just (Right tf) -> unifyTyFunApp tf scope xs b
     _ -> case b of
+      TyApps (TyCon v) ys | Just (Right tf) <- x ^. at v -> SymCo <$> unify scope b ta
+
       TyApps f ys | length xs == length ys -> rethrow ta b $ do
         heads <- unify scope (TyCon v) f
         tails <- traverse (uncurry (unify scope)) (zip xs ys)
         pure (foldl AppCo heads tails)
+
       TyApps f ys | length ys < length xs -> rethrow ta b $ do
-        let (xs_a, xs_b) = splitAt (length ys) xs
+        case f of
+          TyCon{} -> confesses =<< unequal ta b
+          _ -> pure ()
+
+        let ys_l = length ys
+            xs_l = length xs
+            xs_a = take (xs_l - ys_l) xs
+            xs_b = drop (xs_l - ys_l) xs
+
         heads <- unify scope (TyApps (TyCon v) xs_a) f
         tails <- traverse (uncurry (unify scope)) (zip xs_b ys)
         pure (foldl AppCo heads tails)
@@ -675,7 +687,6 @@ unify scope a tb@(TyApps (TyCon _) (_:_)) = rethrow a tb $ SymCo <$> unify scope
 
 unify scope (TyApp f x) (TyApp g y) = AppCo <$> unify scope f g <*> unify scope x y
 
-
 unify _ TyType TyType = pure (ReflCo TyType)
 unify _ a b = confesses =<< unequal a b -- }}}
 

tests/types/unify.ml

@@ -0,0 +1,9 @@
+type sum 'f 'g 'a =
+  | L1 of 'f 'a
+
+type k1 'c 'a = K1 of 'c
+type m1 'f 'a = M1 of 'f 'a
+
+let f x = M1 (L1 (M1 (K1 x)))
+
+let _ = f 123

tests/types/unify.out

@@ -0,0 +1,7 @@
+sum : Infer{'a : type}. Infer{'b : type}. ('b -> type) -> 'a -> 'b -> type
+L1 : Spec{'f : 'b -> type}. Spec{'g : 'a}. Spec{'a : 'b}. 'f 'a -> sum 'f 'g 'a
+k1 : Infer{'a : type}. type -> 'a -> type
+K1 : Spec{'c : type}. Spec{'a : 'a}. 'c -> k1 'c 'a
+m1 : Infer{'a : type}. ('a -> type) -> 'a -> type
+M1 : Spec{'f : 'a -> type}. Spec{'a : 'a}. 'f 'a -> m1 'f 'a
+f : Infer{'a : type}. Infer{'b : 'a}. Infer{'g : 'a}. 'a -> m1 (sum (m1 (k1 'a)) 'g) 'b