Added checks for the assumptions I made on the behaviour of TR concerning phantom types, covariance, contravariance and its ability to recognize different formulations of the same type (or of a subtype or supertype). Updated the mindmap notes.

Graph-notes-copy2.vue

@@ -1,14 +1,14 @@
-<!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2016-12-30 -->
+<!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2017-01-05 -->
 <!-- Tufts VUE: http://vue.tufts.edu/ -->
 <!-- Do Not Remove: VUE mapping @version(1.1) jar:file:/nix/store/z92y35qgs6g3cvvh0i4f14mg5n47zvvi-vue-3.3.0/share/vue/vue.jar!/tufts/vue/resources/lw_mapping_1_1.xml -->
-<!-- Do Not Remove: Saved date Fri Dec 30 22:07:05 CET 2016 by georges on platform Linux 4.4.38 in JVM 1.8.0_122-04 -->
+<!-- Do Not Remove: Saved date Thu Jan 05 00:59:01 CET 2017 by georges on platform Linux 4.4.38 in JVM 1.8.0_122-04 -->
 <!-- Do Not Remove: Saving version @(#)VUE: built October 8 2015 at 1724 by tomadm on Linux 2.6.32-504.23.4.el6.x86_64 i386 JVM 1.7.0_21-b11(bits=32) -->
 <?xml version="1.0" encoding="US-ASCII"?>
 <LW-MAP xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
     xsi:noNamespaceSchemaLocation="none" ID="0"
     label="Graph-notes-copy2.vue" created="1479309847604" x="0.0"
     y="0.0" width="1.4E-45" height="1.4E-45" strokeWidth="0.0" autoSized="false">
-    <resource referenceCreated="1483132025205" size="204773"
+    <resource referenceCreated="1483574341626" size="204773"
         spec="/home/georges/phc/racket-packages/phc-graph/Graph-notes-copy2.vue"
         type="1" xsi:type="URLResource">
         <title>Graph-notes-copy2.vue</title>

test/invariant-phantom-tr-assumptions.rkt

@@ -0,0 +1,42 @@
+#lang typed/racket
+
+(struct A ())
+(struct B A ())
+(struct C A ())
+
+(: f (→ (U 'x A) Void))
+(define (f _) (void))
+
+(let ()
+  (ann f (→ (U B C) Void))
+  (ann f (→ (U 'x B C) Void))
+  (ann f (→ (U 'x C) Void))
+  (ann f (→ (U 'x A C) Void))
+  (ann f (→ (U 'x) Void))
+  (ann f (→ (U) Void))
+  (void))
+
+;;;;;;;;;;
+
+;; Reverse order (BB, CC and DD are more precise invariants than AA)
+(struct AA ())
+(struct BB AA ())
+(struct CC AA ())
+(struct DD AA ())
+
+(define-type (Invariant X) (→ X Void))
+
+(: g (→ (U (Invariant 'x) (Invariant BB) (Invariant CC)) Void))
+(define (g _) (void))
+
+;; Everything works as expected
+(let ()
+  (ann g (→ (U (Invariant BB) (Invariant CC)) Void))
+  (ann g (→ (U (Invariant 'x) (Invariant BB) (Invariant CC)) Void))
+  (ann g (→ (U (Invariant 'x) (Invariant CC)) Void))
+  (ann g (→ (U (Invariant 'x)) Void))
+  (ann g (→ (U) Void))
+  ;; AA works, as it should
+  (ann g (→ (U (Invariant 'x) (Invariant AA) (Invariant CC)) Void))
+  (ann g (→ (U (Invariant 'x) (Invariant AA)) Void))
+  (void))

test/invariant-phantom-tr-assumptions2.rkt

@@ -0,0 +1,69 @@
+#lang typed/racket
+
+(: f (→ (→ (U (Rec R (List (List 'a R)
+                           (List 'b R)))
+              (Rec R (List (List 'a R)
+                           (List 'c R))))
+           Void)
+        Void))
+(define (f x) (void))
+
+(ann f (→ (→ (U (Rec K (List (List 'a K) (List 'c K)))
+                (Rec W (List (List 'a W) (List 'b W))))
+             Void) Void))
+
+(ann f (→ (→ (U (Rec W (List (List 'a W) (List 'b W)))
+                (Rec K (List (List 'a K) (List 'c K))))
+             Void) Void))
+
+(: g (→ (→ (Rec A (Rec B (List (List 'a A)
+                               (List 'b B))))
+           Void)
+        Void))
+(define (g x) (void))
+
+(ann g
+     (→ (→ (Rec B (Rec A (List (List 'a A)
+                               (List 'b B))))
+           Void)
+        Void))
+
+(ann g
+     (→ (→ (Rec X (List (List 'a X)
+                        (List 'b X)))
+           Void)
+        Void))
+
+(define-type (≡ X Y) (List '≡ X Y))
+
+(: h (→ (→ (∀ (X1 X2) (→ (U (≡ (List 'a 'b X1)
+                               (List 'c 'd X1))
+                            (≡ (List 'e 'f X2)
+                               (List 'g 'g X2)))))
+           Void)
+        Void))
+(define (h x) (void))
+
+
+(ann (λ ([x : (Rec R (Pairof 'a (Pairof 'b R)))]) (void))
+       (-> (Rec R (Pairof 'a (Pairof 'b R))) Void))
+
+(ann (λ ([x : (Rec R (Pairof 'a (Pairof 'b R)))]) (void))
+       (-> (Pairof 'a (Rec R (Pairof 'b (Pairof 'a R)))) Void))
+
+(ann (λ ([x : (Rec R (List 'a (List 'b R)))]) (void))
+       (-> (List 'a (Rec R (List 'b (List 'a R)))) Void))
+
+(ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
+       (-> (Rec R (Pairof 'a (Pairof R (Pairof (List 'b R) Null)))) Void))
+
+(ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
+       (-> (Pairof 'a (Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))) Void))
+
+(ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
+       (-> (Pairof 'a (Pairof (Pairof 'a
+                                      (Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))
+                                      )
+                              (Pairof (List 'b (Pairof 'a
+                                                       (Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))
+                                                       )) Null))) Void))