From 095c47c6cb8da6086585d8fb9d6317c34110806e Mon Sep 17 00:00:00 2001 From: Alex Knauth Date: Tue, 25 Apr 2017 13:35:47 -0700 Subject: [PATCH] fix union collapsing (#9) --- turnstile/examples/stlc+union.rkt | 2 +- turnstile/examples/tests/stlc+union+case.rkt | 8 ++++++++ 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 index aaaa384..cf1cc41 100644 --- 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 index 197a531..7957ed0 100644 --- 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 index b98b9a4..7fbcb23 100644 --- 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)