(List (List A ... A) (List A ... A)) does not enforce that the lists have the same length

What version of Racket are you using?

6.8.0.1

What program did you run?

#lang typed/racket

(: f (∀ (A ...) (→ (List (List A ... A) (List A ... A))
                   Void)))
(define (f x) (void))

(f '([1 2 3] [1 2 3]))
;(f '([1 2 3] [1 2 3 4])) ;; rejected, as it should

(define l1 : (Listof Number) '(1 2 3))
(define l2 : (Listof Number) '(1 2 3 4))
(f (list l1 l2)) ;; Should be rejected at run-time, by a contract

What should have happened?

Typed Racket allows passing a Listof where a "dotted-list" (List A ... A) is expected, and this is great!

However, when two Listof are typed as two (List A ... A) with the same bound, I think TR should insert a contract, checking at run-time whether the two lists have the same length, unless the type is a Union also accepting two Listof, or in the example above, if function had the type:

(∀ (B A ...) (case→ (→ (List (List A ... A) (List A ... A)) Void)
                    (→ (Listof B) (Listof B) Void)))`

Another possibility would be to somehow distinguish the (List A ... A) compatible with Listof, and some stronger type which enforces that all PolyDot lists with the same bound have the same length. This would allow programs to guarantee that two lists are of the same length. I see two ways to do this:

• either make (List A ... A) incompatible with Listof, and force the user to write (U (List T ... A) (Listof T)), which means that the type T must be duplicated (a problem when there is a deep tower of those, as the resulting type is exponential in the size of the "specification", a problem I've run into in the past)
• or have two sorts of dotted list types, (Listof A ... A) which is compatible with Listof, and (List A ... A) which is not.

Start by running the typed/racket reproducer from the issue on Racket 6.8.0.1, including the accepted call using l1 and l2 with different lengths. Trace how the two dotted-list bounds are checked at the function boundary; done means the mismatched Listof case is rejected while the accepted compatible cases remain supported.