fix subtyping bug in if; add current-join

tapl/ext-stlc.rkt

@@ -11,7 +11,8 @@
                      [begin/tc begin]
                      [let/tc let] [let*/tc let*] [letrec/tc letrec])
                      ann)
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum))
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum)
+         (for-syntax current-join))
  
 ;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
 ;; Types:
@@ -58,18 +59,20 @@
      #:with e2- (⇑ e2 as Bool)
      (⊢ (or e1- e2-) : Bool)]))
 
+(begin-for-syntax 
+  (define current-join (make-parameter (λ (x y) x))))
 (define-syntax (if/tc stx)
   (syntax-parse stx
     [(_ e_tst e1 e2)
      #:with e_tst- (⇑ e_tst as Bool)
      #:with (e1- τ1) (infer+erase #'e1)
      #:with (e2- τ2) (infer+erase #'e2)
-     ; double check because typing relation may not be reflexive
-     #:fail-unless (or (typecheck? #'τ1 #'τ2)
-                       (typecheck? #'τ2 #'τ1))
-                   (format "branches must have the same type: given ~a and ~a"
+     #:with τ-out ((current-join) #'τ1 #'τ2)
+     #:fail-unless (and (typecheck? #'τ1 #'τ-out)
+                        (typecheck? #'τ2 #'τ-out))
+                   (format "branches have incompatible types: ~a and ~a"
                            (type->str #'τ1) (type->str #'τ2))
-     (⊢ (if e_tst- e1- e2-) : τ1)]))
+     (⊢ (if e_tst- e1- e2-) : τ-out)]))
 
 (define-base-type Unit)
 (define-primop void : (→ Unit))

tapl/stlc+reco+sub.rkt

@@ -52,4 +52,11 @@
          #'([l τl] ...))]
        [_ #f])))
   (current-sub? sub?)
-  (current-typecheck-relation (current-sub?)))
+  (current-typecheck-relation (current-sub?))
+
+  (define (join t1 t2)
+    (cond
+      [((current-sub?) t1 t2) t2]
+      [((current-sub?) t2 t1) t1]
+      [else #'Top]))
+  (current-join join))

tapl/tests/ext-stlc-tests.rkt

@@ -121,7 +121,7 @@
 (typecheck-fail
  (if #t 1 "2")
  #:with-msg 
- "branches must have the same type: given Int and String")
+ "branches have incompatible types: Int and String")
 
 ;; tests from stlc+lit-tests.rkt --------------------------
 ; most should pass, some failing may now pass due to added types/forms

tapl/tests/stlc+reco+sub-tests.rkt

@@ -39,6 +39,13 @@
 ;; this should work! but needs bounded quantification, see fsub.rkt
 (typecheck-fail (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) b))
 
+; conditional
+(check-not-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Nat))
+(check-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Int))
+(check-not-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Nat))
+(check-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Int))
+(check-type (λ ([x : Bool]) (if x "1" 1)) : (→ Bool Top))
+
 ;; previous record tests ------------------------------------------------------
 ;; records (ie labeled tuples)
 (check-type "Stephen" : String)