practical example of keyword parameters with core.typed

Question

Following the wiki of core.typed about keyword parameters, I came up with the following code snippet to test it. I don't see why I am getting the error below.

(ns typeddemo
  (:require [clojure.core.typed :as t]))


(t/ann testfn (Fn [Any & :mandatory {:a t/Num :b t/Num} -> t/Num]
                  [Any & :optional  {:a t/Num :b t/Num} -> t/Str]))

(defn testfn
  [y & {:keys [a b]}]
  (if (and (number? a) (number? b))
    (+ a b)
    "Missing b"))

(testfn 55 :a 5 :b 6)

Static method clojure.lang.Numbers/add could not be applied to arguments:


Domains:
    java.lang.Long java.lang.Long
    java.lang.Double java.lang.Double
    t/AnyInteger t/AnyInteger
    java.lang.Number java.lang.Number

Arguments:
    (t/U Number nil) Number

Ranges:
    java.lang.Long
    java.lang.Double
    t/AnyInteger
    java.lang.Number

with expected type:
    t/Str

in: (clojure.lang.Numbers/add a b)

I had expected that core.typed can infer that when the test (and (number? a) (number? b)) passes, then both arguments must be t/Num and therefore the result should also be t/Num. Only when the test fails, the type is t/Str. Why does it claim that the add function is not applicable. How can the arguments be (t/U Number nil) Number given the condition?