contra

Author: andrew-johnson-4

Makefile

@@ -1,7 +1,7 @@
 CC = cc
 
 dev: install-production
-	lm tests/regress/numerical-pyramid.lsts
+	lm tests/unit/type-inference.lsts
 	$(CC) -O3 tmp.c
 	./a.out
 	#lm tests/c/main.c

SRC/can-unify.lsts

@@ -67,6 +67,11 @@ let can-unify(fpt: Type, pt: Type): U64 = (
           second:rp1
       } => can-unify(lp1,rp1);
 
+      Tuple{
+          first:TGround{tag:c"Arrow", parameters:[lrng.. ldom..]},
+          second:TGround{tag:c"Arrow", parameters:[rrng.. rdom..]}
+      } => can-unify(rdom, ldom) && can-unify(ldom, rdom);
+
       Tuple{
           first:TGround{ltn=tag, lps=parameters},
           second:TGround{rtn=tag, rps=parameters}

tests/unit/type-inference.lsts

@@ -34,3 +34,10 @@ if true {
    let tctx = unify(t-array-x, t-array-A-d);
    assert( substitute(tctx, t-x) == t-A );
 };
+
+let t-f1 = normalize(t3(c"Arrow", t-A, t-A));
+let t-f2 = normalize(t3(c"Arrow", t-C, t-A));
+let t-f3 = normalize(t3(c"Arrow", t-A, t-C));
+
+assert( not(can-unify(t-f2, t-f1)) );
+assert( can-unify(t-f3, t-f1) );