diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
index 7422d9bc0..5700d9f27 100644
--- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
@@ -664,22 +664,10 @@
   (define abs-cases ; used both for abs and magnitude
     (list
      ;; abs is not the identity on negative zeros.
-     ((Un -Zero -PosReal) . -> . (Un -Zero -PosReal) : -true-propset : (-arg-path 0))
-     ;; but we know that we at least get *some* zero, and that it preserves exactness
-     (map unop (list -FlonumZero -SingleFlonumZero -RealZero))
-     ;; abs may not be closed on fixnums. (abs min-fixnum) is not a fixnum
-     ((Un -PosInt -NegInt) . -> . -PosInt)
-     (-Int . -> . -Nat)
-     ((Un -PosRat -NegRat) . -> . -PosRat)
-     (-Rat . -> . -NonNegRat)
-     ((Un -PosFlonum -NegFlonum) . -> . -PosFlonum)
-     (-Flonum . -> . -NonNegFlonum)
-     ((Un -PosSingleFlonum -NegSingleFlonum) . -> . -PosSingleFlonum)
-     (-SingleFlonum . -> . -NonNegSingleFlonum)
-     ((Un -PosInexactReal -NegInexactReal) . -> . -PosInexactReal)
-     (-InexactReal . -> . -NonNegInexactReal)
-     ((Un -PosReal -NegReal) . -> . -PosReal)
-     (-Real . -> . -NonNegReal)))
+     (-> (Un -Zero -PosReal) (Un -Zero -PosReal) : -true-propset : (-arg-path 0))
+     (map unop (list -RealZero -Int -Rat -Flonum -SingleFlonum))
+     (-> (Un -PosReal -NegReal) -PosReal)
+     (-> -Real -NonNegReal)))
 
   ;Check to ensure we fail fast if the flonum bindings change
   (define-namespace-anchor anchor)
@@ -1031,65 +1019,44 @@
     (commutative-case -InexactComplex (Un -InexactComplex -InexactReal -PosRat -NegRat) -InexactComplex)
     (varop N))]
 [+ (from-cases
-    (-> -Zero)
     (-> N N : -true-propset : (-arg-path 0))
-    (binop -Zero)
     (-> N -Zero N : -true-propset : (-arg-path 0))
     (-> -Zero N N : -true-propset : (-arg-path 1))
-    (-> -PosByte -PosByte -PosIndex)
     (-> -Byte -Byte -Index)
-    (-> -PosByte -PosByte -PosByte -PosIndex)
     (-> -Byte -Byte -Byte -Index)
-    (commutative-binop -PosIndex -Index -PosFixnum)
-    (-> -PosIndex -Index -Index -PosFixnum)
-    (-> -Index -PosIndex -Index -PosFixnum)
-    (-> -Index -Index -PosIndex -PosFixnum)
     (-> -Index -Index -NonNegFixnum)
     (-> -Index -Index -Index -NonNegFixnum)
-    (commutative-binop -NegFixnum -One -NonPosFixnum)
-    (commutative-binop -NonPosFixnum -NonNegFixnum -Fixnum)
-    (commutative-case -PosInt -Nat -PosInt)
-    (commutative-case -NegInt -NonPosInt -NegInt)
-    (map varop (list -Nat -NonPosInt -Int))
-    (commutative-case -PosRat -NonNegRat -PosRat)
-    (commutative-case -NegRat -NonPosRat -NegRat)
-    (map varop (list -NonNegRat -NonPosRat -Rat))
-    ;; flonum + real -> flonum
-    (commutative-case -PosFlonum -NonNegReal -PosFlonum)
-    (commutative-case -PosReal -NonNegFlonum -PosFlonum)
-    (commutative-case -NegFlonum -NonPosReal -NegFlonum)
-    (commutative-case -NegReal -NonPosFlonum -NegFlonum)
-    (commutative-case -NonNegFlonum -NonNegReal -NonNegFlonum)
-    (commutative-case -NonPosFlonum -NonPosReal -NonPosFlonum)
-    (commutative-case -Flonum -Real -Flonum)
-    (varop-1+ -Flonum)
-    ;; single-flonum + rat -> single-flonum
-    (commutative-case -PosSingleFlonum (Un -NonNegRat -NonNegSingleFlonum) -PosSingleFlonum)
-    (commutative-case (Un -PosRat -PosSingleFlonum) -NonNegSingleFlonum -PosSingleFlonum)
-    (commutative-case -NegSingleFlonum (Un -NonPosRat -NonPosSingleFlonum) -NegSingleFlonum)
-    (commutative-case (Un -NegRat -NegSingleFlonum) -NonPosSingleFlonum -NegSingleFlonum)
-    (commutative-case -NonNegSingleFlonum (Un -NonNegRat -NonNegSingleFlonum) -NonNegSingleFlonum)
-    (commutative-case -NonPosSingleFlonum (Un -NonPosRat -NonPosSingleFlonum) -NonPosSingleFlonum)
-    (commutative-case -SingleFlonum (Un -Rat -SingleFlonum) -SingleFlonum)
-    (varop-1+ -SingleFlonum)
-    ;; inexact-real + real -> inexact-real
-    (commutative-case -PosInexactReal -NonNegReal -PosInexactReal)
-    (commutative-case -PosReal -NonNegInexactReal -PosInexactReal)
-    (commutative-case -NegInexactReal -NonPosReal -NegInexactReal)
-    (commutative-case -NegReal -NonPosInexactReal -NegInexactReal)
-    (commutative-case -NonNegInexactReal -NonNegReal -NonNegInexactReal)
-    (commutative-case -NonPosInexactReal -NonPosReal -NonPosInexactReal)
-    (commutative-case -InexactReal -Real -InexactReal)
-    ;; real
-    (commutative-case -PosReal -NonNegReal -PosReal)
-    (commutative-case -NegReal -NonPosReal -NegReal)
-    (map varop (list -NonNegReal -NonPosReal -Real -ExactNumber))
-    ;; complex
-    (commutative-case -FloatComplex N -FloatComplex)
-    (commutative-case -Flonum -InexactComplex -FloatComplex)
-    (commutative-case -SingleFlonumComplex (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex)
-    (commutative-case -InexactComplex (Un -Rat -InexactReal -InexactComplex) -InexactComplex)
-    (varop N))]
+    (-> -NegFixnum -One -NonPosFixnum)
+    (-> -One -NegFixnum -NonPosFixnum)
+    (-> -NonPosFixnum -NonNegFixnum -Fixnum)
+    (-> -NonNegFixnum -NonPosFixnum -Fixnum)
+    (-> -Flonum -Real -Flonum)
+    (-> -Real -Flonum -Flonum)
+    (-> -SingleFlonum (Un -Rat -SingleFlonum) -SingleFlonum)
+    (-> (Un -Rat -SingleFlonum) -SingleFlonum -SingleFlonum)
+    (-> -InexactReal -Real -InexactReal)
+    (-> -Real -InexactReal -InexactReal)
+    (-> -FloatComplex N -FloatComplex)
+    (-> N -FloatComplex -FloatComplex)
+    (-> -Flonum -InexactComplex -FloatComplex)
+    (-> -InexactComplex -Flonum -FloatComplex)
+    (-> -SingleFlonumComplex (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex)
+    (-> (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex -SingleFlonumComplex)
+    (-> -InexactComplex (Un -Rat -InexactReal -InexactComplex) -InexactComplex)
+    (-> (Un -Rat -InexactReal -InexactComplex) -InexactComplex -InexactComplex)
+    (-> -PosReal -NonNegReal -PosReal)
+    (-> -NonNegReal -PosReal -PosReal)
+    (-> -PosReal -NonNegReal -NonNegReal -PosReal)
+    (-> -NonNegReal -PosReal -NonNegReal -PosReal)
+    (-> -NonNegReal -NonNegReal -PosReal -PosReal)
+    (-> -NegReal -NonPosReal -NegReal)
+    (-> -NonPosReal -NegReal -NegReal)
+    (-> -NegReal -NonPosReal -NonPosReal -NegReal)
+    (-> -NonPosReal -NegReal -NonPosReal -NegReal)
+    (-> -NonPosReal -NonPosReal -NegReal -NegReal)
+    (map varop (list -Zero -Nat -Int -PosReal -NegReal
+                     -NonNegReal -NonPosReal -Real -ExactNumber N))
+    (map varop-1+ (list -Flonum -SingleFlonum)))]
 
 [- (from-cases
     (binop -Zero)
@@ -1268,45 +1235,28 @@
 
 [add1 (from-cases
        (-> -Zero -One)
-       (-> -One -PosByte)
-       (-> -Byte -PosIndex)
-       (-> -Index -PosFixnum)
-       (-> -NegFixnum -NonPosFixnum)
+       (-> -One -Byte)
+       (-> -Byte -Index)
+       (-> -Index -Fixnum)
        (-> -NonPosFixnum -Fixnum)
-       (-> -Nat -Pos)
        (-> -NegInt -NonPosInt)
-       (unop -Int)
-       (-> -NonNegRat -PosRat)
-       (unop -Rat)
-       (-> -NonNegFlonum -PosFlonum)
-       (unop -Flonum)
-       (-> -NonNegSingleFlonum -PosSingleFlonum)
-       (unop -SingleFlonum)
-       (-> -NonNegInexactReal -PosInexactReal)
-       (unop -InexactReal)
        (-> -NonNegReal -PosReal)
-       (map unop (list -Real -FloatComplex -SingleFlonumComplex -InexactComplex N)))]
+       (-> -InexactReal -InexactReal)
+       (map unop (list -Int -Rat -Flonum -SingleFlonum
+                       -FloatComplex -SingleFlonumComplex
+                       -Real -InexactReal -InexactComplex N)))]
 
 [sub1 (from-cases
        (-> -One -Zero)
        (-> -PosByte -Byte)
        (-> -PosIndex -Index)
-       (-> -Index -Fixnum)
-       (-> -PosFixnum -NonNegFixnum)
        (-> -NonNegFixnum -Fixnum)
        (-> -Pos -Nat)
-       (-> -NonPosInt -NegInt)
-       (unop -Int)
-       (-> -NonPosRat -NegRat)
-       (unop -Rat)
-       (-> -NonPosFlonum -NegFlonum)
-       (unop -Flonum)
-       (-> -NonPosSingleFlonum -NegSingleFlonum)
-       (unop -SingleFlonum)
-       (-> -NonPosInexactReal -NegInexactReal)
-       (unop -InexactReal)
        (-> -NonPosReal -NegReal)
-       (map unop (list -Real -FloatComplex -SingleFlonumComplex -InexactComplex N)))]
+       (map unop (list -Int -Rat -Flonum -SingleFlonum
+                       -Real -InexactReal -FloatComplex
+                       -SingleFlonumComplex -InexactComplex
+                       N)))]
 
 [quotient
  (from-cases
@@ -1498,7 +1448,7 @@
              ;; no positive / negative cases, possible underflow
              (-NonNegReal . -> . -NonNegSingleFlonum)
              (-NonPosReal . -> . -NonPosSingleFlonum)
-             (-Real . -> . -SingleFlonumZero))]
+             (-Real . -> . -SingleFlonum))]
 [real->double-flonum
  (from-cases (map unop all-flonum-types)
              (-SingleFlonumPosZero . -> . -FlonumPosZero)
diff --git a/typed-racket-lib/typed-racket/env/lexical-env.rkt b/typed-racket-lib/typed-racket/env/lexical-env.rkt
index eb12f4f30..5beb01517 100644
--- a/typed-racket-lib/typed-racket/env/lexical-env.rkt
+++ b/typed-racket-lib/typed-racket/env/lexical-env.rkt
@@ -33,7 +33,7 @@
  [lookup-obj-type/lexical ((Object?) (env? #:fail (or/c #f Type? (-> any/c (or/c Type? #f))))
                                      . ->* .
                                      (or/c Type? #f))]
- [lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))])
+ [lookup-alias/lexical ((identifier?) (env?) . ->* . OptObject?)])
 
 ;; used at the top level
 (define (add-props-to-current-lexical! ps)
diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 4f6fbd7b4..9fb28e8c9 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -420,6 +420,19 @@
          (cgen context s t)
          (cgen/seq context t-seq s-seq)))]))
 
+(define/cond-contract (cgen/arrow-pair/arrow context s-arr-pair t-arr)
+  (context? (cons/c Type? Values?) Arrow? . -> . (or/c #f cset?))
+  (match* (s-arr-pair t-arr)
+    [((cons dom1 cdom1)
+      (Arrow: dom2 rst2 kws2 cdom2))
+     (and
+      (null? kws2)
+      (% cset-meet
+         (cgen context cdom1 cdom2)
+         (cgen context
+               (positional-domain->Tuple dom2 rst2)
+               dom1)))]))
+
 (define/cond-contract (cgen/flds context flds-s flds-t)
   (context? (listof fld?) (listof fld?)  . -> . (or/c #f cset?))
   (% cset-meet*
@@ -812,17 +825,35 @@
          (% cset-meet (cg in2 in1) (cg out1 out2))]
         [((Fun: s-arr)
           (Fun: t-arr))
+         (define s-arrow-combinations
+           (let loop ([arrows s-arr]
+                      [acc #f])
+             (match arrows
+               ['() (if acc (list acc) '())]
+               [(cons a rst)
+                (define a* (if acc
+                               (intersect-arrows a acc)
+                               (match a
+                                 [(Arrow: dom rst kws cdom)
+                                  (and (for/and ([kw (in-list kws)])
+                                         (not (Keyword-required? kw)))
+                                       (cons (positional-domain->Tuple dom rst)
+                                             cdom))])))
+                (if a*
+                    (append (loop rst a*)
+                            (loop rst acc))
+                    (loop rst acc))])))
          (% cset-meet*
             (for/list/fail
-             ([t-arr (in-list t-arr)])
-             ;; for each element of t-arr, we need to get at least one element of s-arr that works
-             (let ([results (for*/list ([s-arr (in-list s-arr)]
-                                        [v (in-value (cgen/arrow context s-arr t-arr))]
-                                        #:when v)
-                              v)])
-               ;; ensure that something produces a constraint set
-               (and (not (null? results))
-                    (cset-join results)))))]
+                ([t-arr (in-list t-arr)])
+              ;; for each element of t-arr, we need to get at least one element of s-arr that works
+              (let ([results (for*/list ([s-arr-pair (in-list s-arrow-combinations)]
+                                         [v (in-value (cgen/arrow-pair/arrow context s-arr-pair t-arr))]
+                                         #:when v)
+                               v)])
+                ;; ensure that something produces a constraint set
+                (and (not (null? results))
+                     (cset-join results)))))]
         [(_ _)
          ;; nothing worked, and we fail
          #f]))]))
diff --git a/typed-racket-lib/typed-racket/infer/intersect.rkt b/typed-racket-lib/typed-racket/infer/intersect.rkt
index 7ca62ea81..64f2d3d68 100644
--- a/typed-racket-lib/typed-racket/infer/intersect.rkt
+++ b/typed-racket-lib/typed-racket/infer/intersect.rkt
@@ -236,3 +236,6 @@
     [else (internal-restrict t1 t2 '() obj)]))
 
 (define internal-restrict (intersect-types #f))
+
+
+
diff --git a/typed-racket-lib/typed-racket/rep/object-rep.rkt b/typed-racket-lib/typed-racket/rep/object-rep.rkt
index ff6ebf243..516967f65 100644
--- a/typed-racket-lib/typed-racket/rep/object-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/object-rep.rkt
@@ -37,6 +37,7 @@
          obj-seq-next
          scale-obj
          uninterpreted-PE?
+         intersect-objects
          (rename-out [make-LExp* make-LExp]
                      [make-LExp raw-make-LExp])
          (all-from-out "fme-utils.rkt"))
@@ -395,4 +396,12 @@
 (define (add-path-to-lexp p l)
   (match l
     [(LExp: const terms)
-     (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
\ No newline at end of file
+     (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
+
+
+(define (intersect-objects o1 o2)
+  (match* (o1 o2)
+    [(o o) o]
+    [((Empty:) _) o2]
+    [(_ (Empty:)) o1]
+    [(_ _) o1]))
\ No newline at end of file
diff --git a/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt
index 2cb6cb6a2..d2b323667 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt
@@ -136,7 +136,7 @@
     [stx:exn-body^
      (set! body-results (tc-expr/check #'stx expected))])
   (define handler-results (get-handler-results))
-  (merge-tc-results (cons body-results handler-results)))
+  (union-tc-results (cons body-results handler-results)))
 
 ;; typecheck the expansion of a with-handlers form
 ;; syntax -> void
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
index 78f8b9d68..8d87f1569 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -15,11 +15,14 @@
 (provide/cond-contract
   [tc/funapp1
     ((syntax? stx-list? Arrow? (listof tc-results/c) (or/c #f tc-results/c))
-     (#:check boolean?)
+     (#:check boolean? #:tooltip? boolean?)
      . ->* . full-tc-results/c)])
-(define (tc/funapp1 f-stx args-stx ftype0 arg-ress expected #:check [check? #t])
+(define (tc/funapp1 f-stx args-stx ftype0 arg-ress expected
+                    #:check [check? #t]
+                    #:tooltip? [tooltip? #t])
   ;; update tooltip-table with inferred function type
-  (add-typeof-expr f-stx (ret (make-Fun (list ftype0))))
+  (when tooltip?
+    (add-typeof-expr f-stx (ret (make-Fun (list ftype0)))))
   (match* (ftype0 arg-ress)
     ;; we check that all kw args are optional
     [((Arrow: dom rst (list (Keyword: _ _ #f) ...) rng)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index 9d1d74f89..8bb129320 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -6,7 +6,7 @@
          (utils tc-utils identifier)
          (env tvar-env lexical-env)
          (for-syntax syntax/parse racket/base)
-         (types utils subtype resolve abbrev
+         (types utils subtype resolve abbrev type-table
                 substitute classes prop-ops)
          (typecheck tc-metafunctions tc-app-helper tc-subst tc-envops
                     check-below)
@@ -115,17 +115,14 @@
        ;; check there are no RestDots
        #:when (not (for/or ([a (in-list arrows)])
                      (RestDots? (Arrow-rst a))))
-       (cond
-         ;; find the first function where the argument types match
-         [(ormap (match-lambda
-                   [(and a (Arrow: dom rst _ _))
-                    (and (subtypes/varargs argtys dom rst) a)])
-                 arrows)
-          => (λ (a)
-               ;; then typecheck here -- we call the separate function so that we get
-               ;; the appropriate props/objects
-               (tc/funapp1 f-stx args-stx a args-res expected #:check #f))]
-         [else
+       (define applicable-arrows
+         (filter (match-lambda
+                   [(Arrow: dom rst _ _)
+                    (subtypes/varargs argtys dom rst)])
+                 arrows))
+       
+       (match applicable-arrows
+         [(list)
           ;; if nothing matched, error
           (match arrows
             [(list (Arrow: doms rsts _ rngs) ...)
@@ -135,7 +132,30 @@
               #:msg-thunk (lambda (dom)
                             (string-append
                              "No function domains matched in function application:\n"
-                             dom)))])])]
+                             dom)))])]
+         [(list a) (tc/funapp1 f-stx args-stx a args-res expected #:check #f)]
+         [_
+          ;; call a separate function so that we get
+          ;; the appropriate props/objects
+          (define app-result
+            (intersect-tc-results
+             (for/list ([a (in-list applicable-arrows)])
+               (tc/funapp1 f-stx args-stx a args-res expected
+                           #:check #f
+                           #:tooltip? #f))))
+          (define applicable-domain
+            ;; gather and intersect applicable domains to report to user
+            ;; generally what class of inputs produces the resulting output
+            (for/fold ([domtys (build-list (length argtys) (λ (_) Univ))])
+                      ([a (in-list applicable-arrows)])
+              (match a
+                [(Arrow: dom rst _ _) (for/list ([domty (in-list domtys)]
+                                                 [idx (in-naturals)])
+                                        (intersect domty (dom+rst-ref dom rst idx)))])))
+          (add-typeof-expr
+           f-stx
+           (ret (make-Fun (list (-Arrow applicable-domain (tc-results->values app-result))))))
+          app-result])]
       ;; any kind of dotted polymorphic function without mandatory keyword args
       [(PolyDots: (list fixed-vars ... dotted-var)
                   (Fun: arrows))
@@ -308,7 +328,7 @@
       ;; a union of functions can be applied if we can apply all of the elements
       [(Union: (? Bottom?) ts) #:when (for/and ([t (in-list ts)])
                                         (subtype t top-func))
-       (merge-tc-results
+       (union-tc-results
         (for/list ([fty (in-list ts)])
           (tc/funapp f-stx args-stx fty args-res expected)))]
       ;; bottom or error type is a perfectly good fcn type
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
index 057699b00..9dc9ddbe7 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
@@ -30,7 +30,7 @@
        ;; if there was not any expected results, then merge the 'then'
        ;; and 'else' results so we propogate the correct info upwards
        [(or #f (tc-any-results: #f))
-        (merge-tc-results (list thn-res els-res))]
+        (union-tc-results (list thn-res els-res))]
        ;; otherwise, the subcomponents have already been checked and
        ;; we just return the expected result 'fixed' to replace any
        ;; missing fields (i.e. #f props or objects)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index 72f324132..22c0b6599 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -5,6 +5,7 @@
          racket/match racket/list
          (except-in (types abbrev utils prop-ops)
                     -> ->* one-of/c)
+         (only-in (infer infer) intersect)
          (rep type-rep prop-rep object-rep values-rep rep-utils)
          (typecheck tc-subst)
          (logic ineq)
@@ -12,7 +13,8 @@
 
 (provide abstract-results
          combine-props
-         merge-tc-results
+         union-tc-results
+         intersect-tc-results
          tc-results->values
          erase-existentials)
 
@@ -145,7 +147,7 @@
               (-or p+ p-)])
            tcrs))]))
 
-(define (merge-tc-results results [ignore-propositions? #f])
+(define (union-tc-results results [ignore-propositions? #f])
   (define/match (merge-tc-result r1 r2)
     [((tc-result: t1 (and ps1 (PropSet: p1+ p1-)) o1)
       (tc-result: t2 (PropSet: p2+ p2-) o2))
@@ -165,13 +167,13 @@
      (make-RestDots (Un t1 t2) dbound)])
 
 
-  (define/match (merge-two-results res1 res2)
+  (define/match (union-two-results res1 res2)
     [((tc-result1: (== -Bottom)) res2) res2]
     [(res1 (tc-result1: (== -Bottom))) res1]
-    [((tc-any-results: f1) res2)
-     (-tc-any-results (-or f1 (unconditional-prop res2)))]
-    [(res1 (tc-any-results: f2))
-     (-tc-any-results (-or (unconditional-prop res1) f2))]
+    [((tc-any-results: p1) res2)
+     (-tc-any-results (-or p1 (unconditional-prop res2)))]
+    [(res1 (tc-any-results: p2))
+     (-tc-any-results (-or (unconditional-prop res1) p2))]
     [((tc-results: results1 dty1)
       (tc-results: results2 dty2))
      ;; if we have the same number of values in both cases
@@ -188,7 +190,55 @@
                            (format "~a and ~a." (length results2) (length results1))))])])
 
   (for/fold ([res (ret -Bottom)]) ([res2 (in-list results)])
-    (merge-two-results res res2)))
+    (union-two-results res res2)))
+
+(define (intersect-tc-results results)
+  (define/match (merge-tc-result r1 r2)
+    [((tc-result: t1 (PropSet: p1+ p1-) o1)
+      (tc-result: t2 (PropSet: p2+ p2-) o2))
+     (-tc-result (intersect t1 t2)
+                 (-PS (-and p1+ p2+) (-and p1- p2-))
+                 (match* (o1 o2)
+                   [(o o) o]
+                   [((Empty:) _) o2]
+                   [(_ (Empty:)) o1]
+                   [(_ _) -empty-obj]))])
+
+  (define/match (same-dty? r1 r2)
+    [(#f #f) #t]
+    [((RestDots: t1 dbound) (RestDots: t2 dbound)) #t]
+    [(_ _) #f])
+  (define/match (merge-dty r1 r2)
+    [(#f #f) #f]
+    [((RestDots: t1 dbound) (RestDots: t2 dbound))
+     (make-RestDots (intersect t1 t2) dbound)])
+
+
+  (define/match (intersect-two-results res1 res2)
+    [((tc-result1: (== -Bottom)) res2) (ret -Bottom)]
+    [(res1 (tc-result1: (== -Bottom))) (ret -Bottom)]
+    [((tc-any-results: p1) res2) (add-unconditional-prop res2 p1)]
+    [(res1 (tc-any-results: p2)) (add-unconditional-prop res1 p2)]
+    [((tc-results: results1 dty1) (tc-results: results2 dty2))
+     ;; if we have the same number of values in both cases
+     (cond
+       [(and (= (length results1) (length results2))
+             (same-dty? dty1 dty2))
+        (-tc-results (map merge-tc-result results1 results2)
+                     (merge-dty dty1 dty2))]
+       ;; otherwise, error
+       [else
+        (tc-error/expr "Expected the same number of values, but got ~a"
+                       (if (< (length results1) (length results2))
+                           (format "~a and ~a." (length results1) (length results2))
+                           (format "~a and ~a." (length results2) (length results1))))])])
+
+  (match results
+    [(list r) r]
+    [(cons r rs)
+     (for/fold ([r-acc r])
+               ([r (in-list rs)])
+       (intersect-two-results r-acc r))]))
 
 
 (define (erase-existentials rep)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt
index 12333de89..a0f1975aa 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt
@@ -42,7 +42,7 @@
                      rcvr-type)])]
       ;; union of objects, check pointwise and union the results
       [(Union: (? Bottom?) objs) #:when (andmap Instance? objs)
-       (merge-tc-results (map do-check objs))]
+       (union-tc-results (map do-check objs))]
       [_ (tc-error/expr/fields
           "send: type mismatch"
           "expected" "an object"
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 09834e3b0..6527d7b41 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -21,13 +21,13 @@
                     one-of/c))
 
 (lazy-require
- ("../infer/infer.rkt" (infer))
+ ("../infer/infer.rkt" (infer intersect))
  ("prop-ops.rkt" (-and))
  ("../typecheck/tc-subst.rkt" (instantiate-obj+simplify))
  ("../typecheck/tc-envops.rkt" (env+ implies-in-env?)))
 
 
-(provide NameStruct:)
+(provide NameStruct: positional-domain->Tuple)
 
 (provide/cond-contract
  [subtype (->* (Type? Type?) ((or/c #f OptObject?)) boolean?)]
@@ -39,7 +39,8 @@
                        (listof Type?)
                        (or/c Type? Rest? #f)
                        boolean?)]
- [unrelated-structs (-> Struct? Struct? boolean?)])
+ [unrelated-structs (-> Struct? Struct? boolean?)]
+ [intersect-arrows (-> Arrow? Arrow? (or/c #f (cons/c Type? Values?)))])
 
 
 ;; When subtype is called w/ no object, we
@@ -186,7 +187,7 @@
 ;; NOTE: This function takes into account that domains are
 ;; contravariant w.r.t. subtyping, i.e. callers should NOT
 ;; flip argument order.
-(define/cond-contract (Arrow-domain-subtypes* A dom1 rst1 dom2 rst2 [objs #f])
+(define/cond-contract (positional-domain-subtypes* A dom1 rst1 dom2 rst2 [objs #f])
   (->* (list?
         (listof Type?)
         (or/c #f Rest? RestDots?)
@@ -198,12 +199,26 @@
     [((cons t1 ts1) (cons t2 ts2))
      (subtype-seq A
                   (subtype* t2 t1 (and objs (car objs)))
-                  (Arrow-domain-subtypes* ts1 rst1 ts2 rst2 (and objs (cdr objs))))]
+                  (positional-domain-subtypes* ts1 rst1 ts2 rst2 (and objs (cdr objs))))]
     [(_ _)
      (subtype* A
                (-Tuple* dom2 (Rest->Type rst2))
                (-Tuple* dom1 (Rest->Type rst1)))]))
 
+(define/cond-contract (Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2 [objs #f])
+  (->* (list?
+        (listof Type?)
+        (or/c #f Rest? RestDots?)
+        (listof Keyword?)
+        (listof Type?)
+        (or/c #f Rest? RestDots?)
+        (listof Keyword?))
+       ((listof Object?))
+       (or/c #f list?))
+  (subtype-seq A
+               (positional-domain-subtypes* dom1 rst1 dom2 rst2 objs)
+               (kw-subtypes* kws1 kws2)))
+
 (define-syntax-rule (with-fresh-ids len ids . body)
   (let-values ([(ids seq) (for/fold ([ids '()]
                                      [seq (temp-ids)])
@@ -213,27 +228,33 @@
     (parameterize ([temp-ids seq])
       . body)))
 
-;; simple co/contra-variance for ->
-(define/cond-contract (arrow-subtype* A arr1 arr2)
-  (-> list? Arrow? Arrow? (or/c #f list?))
-  (match* (arr1 arr2)
-    [((Arrow: dom1 rst1 kws1 raw-rng1)
-      (Arrow: dom2 rst2 kws2 raw-rng2))
-     (define A* (subtype-seq A
-                             (Arrow-domain-subtypes* dom1 rst1 dom2 rst2)
-                             (kw-subtypes* kws1 kws2)))
-     (cond
-       [(not A*) #f]
-       [else
-        (with-fresh-ids (length dom2) ids
-          (define mapping
-            (for/list ([idx (in-naturals)]
-                       [id (in-list ids)]
-                       [t (in-list dom2)])
-              (list* idx id t)))
-          (subval* A*
-                   (instantiate-obj+simplify raw-rng1 mapping)
-                   (instantiate-obj raw-rng2 ids)))])]))
+;; A <: C₁ ∩ ... ∩ Cₙ
+;; D₁ ∩ ... ∩ Dₙ <: B
+;; ------------------------
+;; (C₁→D₁∩...∩Cₙ→Dₙ) <: A→B
+(define/cond-contract (arrows/arrow-subtype* A arrows1 arrow2)
+  (-> list? (listof Arrow?) Arrow? (or/c #f list?))
+  (match-define (Arrow: dom2 rst2 kws2 raw-cdom2) arrow2)
+  (define raw-cdom1
+    (for/fold ([cdom #f])
+              ([a1 (in-list arrows1)])
+      (match-define (Arrow: dom1 rst1 kws1 raw-cdom1) a1)
+      (cond
+        [(Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2)
+         (if cdom (intersect-values cdom raw-cdom1) raw-cdom1)]
+        [else cdom])))
+  (cond
+    [(not raw-cdom1) #f]
+    [else
+     (with-fresh-ids (length dom2) ids
+       (define mapping
+         (for/list ([idx (in-naturals)]
+                    [id (in-list ids)]
+                    [t (in-list dom2)])
+           (list* idx id t)))
+       (subval* A
+                (instantiate-obj+simplify raw-cdom1 mapping)
+                (instantiate-obj raw-cdom2 ids)))]))
 
 
 ;; is an Arrow a subtype of a DepFun?
@@ -254,7 +275,7 @@
                       (instantiate-obj d ids)))
        (define A* (subtype-seq A
                                (kw-subtypes* kws1 '())
-                               (Arrow-domain-subtypes* dom1 rst1 dom2 #f (map -id-path ids))))
+                               (positional-domain-subtypes* dom1 rst1 dom2 #f (map -id-path ids))))
        (cond
          [(not A*) #f]
          [else
@@ -310,7 +331,7 @@
   (define rst (match raw-rst
                 [(? Type?) (make-Rest (list raw-rst))]
                 [_ raw-rst]))
-  (Arrow-domain-subtypes* A dom rst argtys #f))
+  (positional-domain-subtypes* A dom rst argtys #f))
 
 
 ;;************************************************************
@@ -805,18 +826,18 @@
    (match* (t2 arrows1)
      ;; special case when t1 can be collapsed into simpler arrow
      [((Fun: (list arrow2)) (app collapsable-arrows? (? Arrow? arrow1)))
-      (arrow-subtype* A arrow1 arrow2)]
+      (arrows/arrow-subtype* A (list arrow1) arrow2)]
      ;; special case when t1 can be collapsed into simpler arrow
      [((? DepFun? dfun) (app collapsable-arrows? (? Arrow? arrow1)))
       (arrow-subtype-dfun* A arrow1 dfun)]
      [((Fun: arrows2) _)
       (cond
         [(null? arrows1) #f]
-        [else (for/fold ([A A])
-                        ([a2 (in-list arrows2)]
-                         #:break (not A))
-                (for/or ([a1 (in-list arrows1)])
-                  (arrow-subtype* A a1 a2)))])]
+        [else
+         (for/fold ([A A])
+                   ([a2 (in-list arrows2)]
+                    #:break (not A))
+           (arrows/arrow-subtype* A arrows1 a2))])]
      [((? DepFun? dfun) _)
       (for/or ([a1 (in-list arrows1)])
         (arrow-subtype-dfun* A a1 dfun))]
@@ -1229,3 +1250,70 @@
      #false]
     [_ (continue<: A t1 t2 obj)])]
   [else: (continue<: A t1 t2 obj)])
+
+
+;; intersects two monomorphic Values (i.e. see rep/values-rep)
+;; if the values are strictly incompatible, we return ⊥,
+(define (intersect-values v1 v2)
+  (match* (v1 v2)
+    [(v v) v]
+    [((ValuesDots: rs1 dty1 dbound)
+      (ValuesDots: rs2 dty2 dbound))
+     (make-ValuesDots (map intersect-results rs1 rs2) (intersect dty1 dty2) dbound)]
+    [((? ValuesDots?) _) v1]
+    [(_ (? ValuesDots?)) v2]
+    [((AnyValues: p1) (AnyValues: p2)) (make-AnyValues (-and p1 p2))]
+    [((AnyValues: p) (Values: (cons (Result: t (PropSet: p+ p-) o) rst)))
+     (make-Values (cons (make-Result t (-PS (-and p p+) (-and p p-)) o) rst))]
+    [((Values: (cons (Result: t (PropSet: p+ p-) o) rst)) (AnyValues: p))
+     (make-Values (cons (make-Result t (-PS (-and p p+) (-and p p-)) o) rst))]
+    [((Values: rs1) (Values: rs2))
+     (cond
+       [(= (length rs1) (length rs2))
+        (make-Values (map intersect-results rs1 rs2))]
+       [else (-values -Bottom (-PS -ff -ff) -empty-obj)])]))
+
+;; intersects two Results (i.e. see rep/core-rep.rkt) pointwise
+(define (intersect-results r1 r2)
+  (match* (r1 r2)
+    [((Result: t1 (PropSet: p1+ p1-) o1)
+      (Result: t2 (PropSet: p2+ p2-) o2))
+     (make-Result (intersect t1 t2) (-PS (-and p1+ p2+) (-and p1- p2-)) (intersect-objects o1 o2))]))
+
+
+(define (positional-domain->Tuple dom rst)
+  (-Tuple* dom (or (and rst (Rest->Type rst))
+                   -Null)))
+
+(define (intersect-arrows arrow1 arrow2)
+  (match* (arrow1 arrow2)
+    [((cons dom1 cdom1) (cons dom2 cdom2))
+     (define dom (intersect dom1 dom2))
+     (cond
+       [(Bottom? dom) #f]
+       [else (cons dom (intersect-values cdom1 cdom2))])]
+    [((Arrow: dom1 rst1 kws1 cdom1)
+      (Arrow: dom2 rst2 kws2 cdom2))
+     #:when (and (andmap (λ (kw) (not (Keyword-required? kw))) kws1)
+                 (andmap (λ (kw) (not (Keyword-required? kw))) kws2))
+     (define dom (intersect (positional-domain->Tuple dom1 rst1)
+                            (positional-domain->Tuple dom2 rst2)))
+     (cond
+       [(Bottom? dom) #f]
+       [else (cons dom (intersect-values cdom1 cdom2))])]
+    [((cons dom1 cdom1)
+      (Arrow: dom2 rst2 kws2 cdom2))
+     #:when (andmap (λ (kw) (not (Keyword-required? kw))) kws2)
+     (define dom (intersect dom1 (positional-domain->Tuple dom2 rst2)))
+     (cond
+       [(Bottom? dom) #f]
+       [else (cons dom (intersect-values cdom1 cdom2))])]
+    [((Arrow: dom1 rst1 kws1 cdom1)
+      (cons dom2 cdom2))
+     #:when (andmap (λ (kw) (not (Keyword-required? kw))) kws1)
+     (define dom (intersect (positional-domain->Tuple dom1 rst1)
+                            dom2))
+     (cond
+       [(Bottom? dom) #f]
+       [else (cons dom (intersect-values cdom1 cdom2))])]
+    [(_ _) #f]))
diff --git a/typed-racket-lib/typed-racket/types/type-table.rkt b/typed-racket-lib/typed-racket/types/type-table.rkt
index ba354330f..565e9eeba 100644
--- a/typed-racket-lib/typed-racket/types/type-table.rkt
+++ b/typed-racket-lib/typed-racket/types/type-table.rkt
@@ -67,13 +67,13 @@
               ;; the car should be the latest stx for the location
               (if (equal? e (car seen))
                   ;; combine types seen at the latest
-                  (tooltip seen (merge-tc-results (list t results) #t))
+                  (tooltip seen (union-tc-results (list t results) #t))
                   old)
               (tooltip (cons e seen) t))]))
      #f))
   (hash-update! type-table e
                 (λ (prev) (cond
-                            [prev (merge-tc-results (list t prev) #t)]
+                            [prev (union-tc-results (list t prev) #t)]
                             [else t]))
                 #f))
 
diff --git a/typed-racket-lib/typed-racket/types/utils.rkt b/typed-racket-lib/typed-racket/types/utils.rkt
index 139f3ac77..acd2508d4 100644
--- a/typed-racket-lib/typed-racket/types/utils.rkt
+++ b/typed-racket-lib/typed-racket/types/utils.rkt
@@ -34,6 +34,7 @@
          [(Rest: rst-ts) (list-ref rst-ts (remainder idx (length rst-ts)))]
          [_ (if (procedure? default) (default) default)])]))
 
+
 (define (Rest->Type r)
   (match r
     [#f -Null]
diff --git a/typed-racket-test/unit-tests/metafunction-tests.rkt b/typed-racket-test/unit-tests/metafunction-tests.rkt
index 4dde69dad..01a3c7c8d 100644
--- a/typed-racket-test/unit-tests/metafunction-tests.rkt
+++ b/typed-racket-test/unit-tests/metafunction-tests.rkt
@@ -75,33 +75,33 @@
        #t)
     )
 
-    (test-suite "merge-tc-results"
+    (test-suite "union-tc-results"
       (check-equal?
-        (merge-tc-results (list))
+        (union-tc-results (list))
         (ret -Bottom))
       (check-equal?
-        (merge-tc-results (list (ret Univ)))
+        (union-tc-results (list (ret Univ)))
         (ret Univ))
       (check-equal?
-        (merge-tc-results (list (ret Univ -tt-propset (make-Path null #'x))))
+        (union-tc-results (list (ret Univ -tt-propset (make-Path null #'x))))
         (ret Univ -tt-propset (make-Path null #'x)))
       (check-equal?
-        (merge-tc-results (list (ret -Bottom) (ret -Symbol -tt-propset (make-Path null #'x))))
+        (union-tc-results (list (ret -Bottom) (ret -Symbol -tt-propset (make-Path null #'x))))
         (ret -Symbol -tt-propset (make-Path null #'x)))
       (check-equal?
-        (merge-tc-results (list (ret -String) (ret -Symbol)))
+        (union-tc-results (list (ret -String) (ret -Symbol)))
         (ret (Un -Symbol -String)))
       (check-equal?
-        (merge-tc-results (list (ret -String -true-propset) (ret -Symbol -true-propset)))
+        (union-tc-results (list (ret -String -true-propset) (ret -Symbol -true-propset)))
         (ret (Un -Symbol -String) -true-propset))
       (check-equal?
-        (merge-tc-results (list (ret (-val #f) -false-propset) (ret -Symbol -true-propset)))
+        (union-tc-results (list (ret (-val #f) -false-propset) (ret -Symbol -true-propset)))
         (ret (Un -Symbol (-val #f)) -tt-propset))
       (check-equal?
-        (merge-tc-results (list (ret (list (-val 0) (-val 1))) (ret (list (-val 1) (-val 2)))))
+        (union-tc-results (list (ret (list (-val 0) (-val 1))) (ret (list (-val 1) (-val 2)))))
         (ret (list (Un (-val 0) (-val 1)) (Un (-val 1) (-val 2)))))
       (check-equal?
-        (merge-tc-results (list (ret null null null -Symbol 'x) (ret null null null -String 'x)))
+        (union-tc-results (list (ret null null null -Symbol 'x) (ret null null null -String 'x)))
         (ret null null null (Un -Symbol -String) 'x))
     )
 
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index 7cb49dd38..9fe4667f3 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -465,7 +465,7 @@
         (tc-e (lcm (ann 3 Integer) 1/2) -NonNegRat)
         (tc-e (lcm (ann 3 Integer) -1/2) -NonNegRat)
         (tc-e (expt 0.5 0.3) -NonNegFlonum)
-        (tc-e (expt 0.5 2) (t:Un -NonNegFlonum -One))
+        (tc-e (expt 0.5 2) -NonNegFlonum)
         (tc-e (expt 0.5 0) -One)
         (tc-e (expt -1/2 -1/2) -Number)
         (tc-e (expt (ann 0.5 Float) (ann 2 Natural)) -Real)
@@ -535,7 +535,7 @@
         (tc-e (/ (round (exact-round -2.7393196f0)) (real->double-flonum (inexact->exact (real->single-flonum -0.0)))) -Real)
         (tc-e (bitwise-and (exact-round 1.7976931348623157e+308) (exact-round -29)) -Int)
         (tc-e (flexpt -0.0 -1.0) -Flonum)
-        (tc-e (expt -0.0f0 -3.0) -Real)
+        (tc-e (expt -0.0f0 -3.0) -InexactReal)
         (tc-e (expt -8.665778974912815f+107 -677460115195106837726964554590085563061636191189747) -Number)
         (tc-e (expt (sin +inf.f) +nan.0+nan.0i) -Number)
         (tc-e (/ (gcd 1 0) -0.0f0 2.718281828459045) -Real)