I have some ideas for supporting multiple dotted variables. partial is the most obvious usage.
cc/partial
;; current type
(t/All [y a b c d z :..]
(t/IFn [[z :.. z :-> y] :-> [z :.. z :-> y]]
[[a z :.. z :-> y] a :-> [z :.. z :-> y]]
[[a b z :.. z :-> y] a b :-> [z :.. z :-> y]]
[[a b c z :.. z :-> y] a b c :-> [z :.. z :-> y]]
[[a b c d z :.. z :-> y] a b c d :-> [z :.. z :-> y]]
[[a :* :-> y] a :* :-> [a :* :-> y]]))
;; generalized type
#_
(t/All [r b1 :.. b2 :..]
[[b1 :.. b1 b2 :.. b2 :-> r] b1 :.. b1 :-> [b2 :.. b2 :-> r]])
the problem is inferring b1 :.. b1 b2 :.. b2 in isolation is not possible since we don't know where the b1's end and b2's start. we first need to populate the b1s by looking at the next arguments to partial. I think this is a simple as delaying inference for any argument that has multiple dots (just need to add another heuristic to the inference ordering logic).
the other problem is that t/inst cannot deal with multiple dotted variables. to instantiate the current dotted type you give a flat list of types like (t/inst partial Y A B C D Z0 Z1 Z2 Z3). This will need to change to (t/inst partial Y A B C D (t/cat Z0 Z1 Z2 Z3)). then we can provide arguments to the new type like this: (t/inst partial R (t/cat B1_0 B2_1 B2_2) (t/cat B2_0 B2_1 B2_2)).
Seems possible to support both styles if there's just a single dotted variable so it might not have to be a breaking change.