This is a minimal example of the function that I can't get to typecheck:
(: int-sequence-to-vector ((Sequenceof Integer) -> (Vectorof Integer)))
(define (int-sequence-to-vector seq)
(cond
[(vector? seq) seq] ; This line is the problem.
[else (for/vector : (Vectorof Integer) ([v seq]) v)]))
The goal is to preserve the type of the elements of the sequence (so, the function range should be -> (Vectorof Integer) rather than -> Vectortop) and to make operating on vectors a no-op.
The error is:
Type Checker: type mismatch
expected: (Vectorof Integer)
given: (∩ (Sequenceof Integer) VectorTop) in: seq
I'm not sure what the difference is between VectorTop and (Vectorof Any), and it also seems to me that a (Sequenceof T) that is also a VectorTop must be a (Vectorof T).
The following adds a cast around the value:
(: int-sequence-to-vector ((Sequenceof Integer) -> (Vectorof Integer)))
(define (int-sequence-to-vector seq)
(cond
[(vector? seq) (cast seq (Vectorof Integer))]
[else (for/vector : (Vectorof Integer) ([v seq]) v)]))
But that doesn't help:
Type Checker: Type (∩ (Sequenceof Integer) VectorTop) could not be
converted to a contract:
Intersection type contract contains more than 1 non-flat contract:
(∩ (Sequenceof Integer) VectorTop) in: seq
This might seem weird at first, but things are very different because vectors are mutable.
If something is a (Sequenceof Integer), that only means that when you get an element from it it's an integer. But the type (Vectorof Integer) means that and something more. It means that when you set an element, you're allowed to set it to any integer you want.
(: mutate-vector-of-integer : (Vectorof Integer) -> Void)
(define (mutate-vector-of-integer voi)
(vector-set! voi 0 -987654321)) ; can set it to any integer
Because of this, typechecking with vectors has to be stricter than with sequences.
For example, with sequences you can pass a (Sequenceof Byte) to a function expecting a (Sequenceof Integer) and it's no problem. Even passing a (Vectorof Byte) to a function expecting a (Sequenceof Integer) is fine, but only because Sequenceof by itself doesn't allow you to mutate the sequence.
However, using a (Vectorof Byte) as a (Vectorof Integer) can't be allowed because of the possibility of mutation. The technical term for this is that Vectorof is invariant.
(define vob : (Vectorof Byte)
(vector 1 2 3))
(expect-vector-of-integer vob)
;Type Checker: type mismatch
; expected: (Vectorof Integer)
; given: (Vectorof Byte) in: vob
This is also why VectorTop is different from (Vectorof Any). The type (Vectorof Any) tells you two things: when you get an element it has type Any, and that when you set an element you're allowed to use Any. In contrast, the type VectorTop doesn't give you any of the "set" information, so VectorTop by itself doesn't allow mutation.