Two limited collection types are disjoint if their base types
    are disjoint, or their element types are not equivalent, or
    their sizes are not compatible. ...

I believe that should read:

    Two limited collection types are disjoint if their base types
    are disjoint, or their element types are disjoint, or their
    sizes are not compatible.

The reason should be clear from
< http://www.*-*-*.com/ #HEADIN...>.

--
Ashley Yakeley, Seattle WA

  T1 = C1[E1]
  T2 = C2[E2]

  T1 <= T2 iff C1 <= C2 && E1 == E2

As a result, a limited collection type T1 can only be a subtype of some
other limited collection type T2 if they have equivalent element types.
If they have different element types, then they are disjoint by definition.

Some other languages have used a different subtyping rule for parameterized
types (the more usual name for such things).  In particular, I seem to
recall Eiffel's rule is different and allows one of the contained types to
be a subtype of the other (I think if E1 <= E2, with the possibility of
required runtime checks for some operations if E1 != E2, but I could be
misremembering).

The following paper:
  "Subtypes vs Where Clauses: Constraining Parametric Polymorphism"
  Mark Day, Robert Gruber, Barbara Liskov, Andrew C. Myers, OOPSLA95
gives good arguments for why subtype for parameterized types should require
equivalent contained types (see section 4 of the paper).  Note that this
paper has nothing directly to do with Dylan, it just happened to provide
some good formal arguments for a decision that had already been made for
Dylan (after lengthy discussion, and for some of the same reasons given
in that paper).

A collection of integers is not a collection of objects: the latter
typically allows you to add any object to it, which the former does not.
Perhaps that would sound more intuitive if I said 'collection that can
hold any integer and only integers', etc.

--
Ashley Yakeley, Seattle WA