diff --git a/collects/tests/typed-racket/succeed/pr12905.rkt b/collects/tests/typed-racket/succeed/pr12905.rkt
new file mode 100644
index 00000000..9644b270
--- /dev/null
+++ b/collects/tests/typed-racket/succeed/pr12905.rkt
@@ -0,0 +1,22 @@
+#lang typed/racket
+
+(: f1 (case-> (Number -> Number) (Number 4 -> Number)))
+(define (f1 x (y 4)) y)
+
+(f1 2 4)
+
+(: f2 (4 -> (Values Number Number)))
+(define (f2 x) (values x x))
+
+(f2 4)
+
+(: f3 (4 Number * -> Number))
+(define (f3 x . y) x)
+
+(f3 4)
+
+(: f4 (4 * -> Number))
+(define (f4 . y) 5)
+
+(f4 4 4)
+
diff --git a/collects/tests/typed-racket/xfail/expectations.rkt b/collects/tests/typed-racket/xfail/expectations.rkt
new file mode 100644
index 00000000..54b8059a
--- /dev/null
+++ b/collects/tests/typed-racket/xfail/expectations.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket
+
+
+(: f1 ((U 4 'four) -> Boolean : Number))
+(define (f1 x) (number? x))
+(f1 4)
+
+(: f2 (All (b ...) (b ... b -> Number)))
+(define (f2 . y)
+  (: f2-inner (4 b ... b -> Number))
+  (define (f2-inner x . z) 5)
+  (apply f2-inner 4 y))
diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt
index 3561a3ee..cb4e5d91 100644
--- a/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt
+++ b/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt
@@ -5,7 +5,7 @@
          "utils.rkt"
          syntax/parse racket/match 
          syntax/parse/experimental/reflect
-         (typecheck signatures tc-funapp tc-app-helper)
+         (typecheck signatures tc-funapp tc-app-helper tc-subst)
          (types utils abbrev)
          (rep type-rep filter-rep object-rep rep-utils)
          (for-template racket/base))
@@ -57,23 +57,56 @@
 
 
 
+;; TODO: handle drest, and filters/objects
+(define (arr-matches? arr args)
+  (match arr
+    [(arr: domain
+           (Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:)) ...))
+           rest #f (list (Keyword: _ _ #f) ...))
+     (cond
+       [(< (length domain) (length args)) rest]
+       [(= (length domain) (length args)) #t]
+       [else #f])]
+    [_ #f]))
+
+(define (has-filter? arr)
+  (match arr
+    [(arr: _ (Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:)) ...))
+           _ _ (list (Keyword: _ _ #f) ...)) #f]
+    [else #t]))
+
+
 (define (tc/app-regular form expected)
   (syntax-case form ()
     [(f . args)
      (let* ([f-ty (single-value #'f)]
             [args* (syntax->list #'args)])
-       (match f-ty
-         [(tc-result1:
-           (and t (Function:
-                   (list (and a (arr: (? (λ (d) (= (length d) (length args*))) dom)
-                                      (Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:))))
-                                      #f #f (list (Keyword: _ _ #f) ...)))))))
-          (for ([a (in-list args*)] [t (in-list dom)])
-            (tc-expr/check a (ret t)))
-          (ret v)]
-         [_
-          (let ([arg-tys (map single-value (syntax->list #'args))])
-            (tc/funapp #'f #'args f-ty arg-tys expected))]))]))
+       (define (matching-arities arrs)
+         (for/list ([arr (in-list arrs)] #:when (arr-matches? arr args*)) arr))
+       (define (has-drest/filter? arrs)
+         (for/or ([arr arrs])
+           (or (has-filter? arr) (arr-drest arr))))
+
+       (define arg-tys
+         (match f-ty
+           [(tc-result1: (Function: (? has-drest/filter?)))
+            (map single-value args*)]
+           [(tc-result1:
+             (Function:
+               (app matching-arities
+                 (list (arr: doms ranges rests drests _) ..1))))
+            (define matching-domains
+              (in-values-sequence
+                (apply in-parallel
+                  (for/list ((dom (in-list doms)) (rest (in-list rests)))
+                    (in-sequences (in-list dom) (in-cycle (in-value rest)))))))
+            (for/list ([a (in-list args*)] [types matching-domains])
+              (match-define (cons t ts) types)
+              (if (for/and ((t2 ts)) (equal? t t2))
+                  (tc-expr/check a (ret t))
+                  (single-value a)))]
+           [_ (map single-value args*)]))
+       (tc/funapp #'f #'args f-ty arg-tys expected))]))
 
 ;(trace tc/app/internal)