logical simplification during type checking is incomplete

The type environment and logical propositions are not as thoroughly combined as they should be when type checking. This leads to some programs---which appear to be Typed Racket's "bread and butter" when it comes to checking---to fail for no good reason:

#lang typed/racket


(define real-real : (-> Real Real Boolean)
  (λ (a b) #t))
(define real-bool : (-> Real Boolean Boolean)
  (λ (a b) #t))
(define bool-real : (-> Boolean Real Boolean)
  (λ (a b) #t))
(define bool-bool : (-> Boolean Boolean Boolean)
  (λ (a b) #t))


(: f (-> (U Real Boolean) (U Real Boolean) Boolean))
(define (f l r)
  (cond
    [(and (real? l) (real? r))
     (real-real l r)]
    [(and (boolean? l) (real? r))
     (bool-real l r)]
    [(and (real? l)    (boolean? r))
     (real-bool l r)]
    [else
     (bool-bool l r)])) ;; <- fails to type check with message:

;Type Checker: type mismatch
;  expected: Boolean
;  given: (U Real Boolean) in: r

This program should easily type check, but because of some subtle design choices in implementing some logical algorithms, it does not. In principle this should be an easy fix, but we will need to experiment and tinker to make sure we choose the "right" easy fix.

More details: In the above program, in the else-clause the type checking context contains more-or-less the following information:

• Type environment [x : Str, y : Str U Bool]
• Prop environment [(x is not a Bool), ((x is not a Str) OR (y is not a Bool))]

Because (unfortunately) the current way logical information is combined to derived new facts only uses propositions and not the explicit "type environment" (see combine-props in the implementation) we do not also deduce that y is a Bool.

I've looked into this a little -- simply adding more propositions when we extend a context this does not solve the problem, since update (the function which combines type info for the same identifier) is not used in combine-props.

I think the ultimate solution should be to have combine-props (or a similar function) simply use the type environment and not try to only work with the list of propositions when performing those logical simplifications.