www

commit 095c47c6cb8da6086585d8fb9d6317c34110806e
parent bbcdfaf9cf0c7869e59ab6ec039f9786ed4effe7
Author: Alex Knauth <alexander@knauth.org>
Date:   Tue, 25 Apr 2017 13:35:47 -0700

fix union collapsing (#9)


Diffstat:
M
turnstile/examples/stlc+union.rkt
 | 
2
+-
M
turnstile/examples/tests/stlc+union+case.rkt
 | 
8
++++++++
M
turnstile/examples/tests/stlc+union.rkt
 | 
8
++++++++

3 files changed, 17 insertions(+), 1 deletion(-)
diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt
@@ -58,7 +58,7 @@
      #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys)
      #:with tys- (prune+sort #'(ty1- ... ... ty2- ...))
      (if (= 1 (stx-length #'tys-))
-         (stx-car #'tys)
+         (stx-car #'tys-)
          #'(U* . tys-))]))
 (define-syntax Bool
   (make-variable-like-transformer
diff --git a/turnstile/examples/tests/stlc+union+case.rkt b/turnstile/examples/tests/stlc+union+case.rkt
@@ -37,6 +37,14 @@
 (define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat))))
 (check-type ((λ ([x : NNN]) x) 1) : Nat -> 1)
 
+; check that pruning and collapsing don't throw away types when the union
+; contains another empty union
+(typecheck-fail
+ (λ ([x : (U (U) String)])
+   (ann x : (U)))
+ #:with-msg
+ "expected \\(U\\), given \\(U \\(U\\) String\\)")
+
 
 ;; tests from stlc+sub ---------------------
 (check-type 1 : Num)
diff --git a/turnstile/examples/tests/stlc+union.rkt b/turnstile/examples/tests/stlc+union.rkt
@@ -27,6 +27,14 @@
 (define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat))))
 (check-type ((λ ([x : NNN]) x) 1) : Nat -> 1)
 
+; check that pruning and collapsing don't throw away types when the union
+; contains another empty union
+(typecheck-fail
+ (λ ([x : (U (U) String)])
+   (ann x : (U)))
+ #:with-msg
+ "expected \\(U\\), given \\(U \\(U\\) String\\)")
+
 
 ;; tests from stlc+sub ---------------------
 (check-type 1 : Num)