Merge pull request #1282 from andrew-johnson-4/contravariance-arrows

Contravariance arrows

Author: andrew-johnson-4

BOOTSTRAP/cli.c

@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.20.57"
+version = "1.20.58"
 authors = ["Andrew <andrew@subarctic.org>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

Cargo.toml

@@ -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

Makefile

@@ -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}

SRC/can-unify.lsts

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

SRC/unify.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) );