Soundness of Excluded-type composition in paper?

[Blaisorblade]

I was finally reading the spores paper from https://infoscience.epfl.ch/record/191239/files/spores_1.pdf (which IIUC is still the up-to-date documentation since it's not subsumed by the SIP).

I like the approach, but one issue made me wonder about typing of spores composition and Excluded, so I thought I'd ask @heathermiller and @phaller.

I might be missing something, also because I've been skimming the paper a bit, but I've looked for explanations in a couple of obvious places and found none.
Also, this issue appears in a part of the type system that is formalized but not proven correct (I've also checked with https://infoscience.epfl.ch/record/191240/files/spores-formally.pdf, and there is no difference).

Take the example in Sec. 2.4. What happens if we have MyActor <: Actor,

type T1 = Spore[Int, String] {
  type Captured = (Int, Util)
  type Excluded = No[Actor]
}
type T2 = Spore[String, Int] {
  type Captured = (MyActor, Int)
  type Excluded = No[Util]
}

then have s1: S1, s2: S2 and compute the type S3 of s3 = s1 compose s2

Applying the rules in the paper, as I understand them, I get the incorrect result:

type T3 = Spore[String, String] {
  type Captured = (Int, Util, MyActor, Int)
  type Excluded = No[Actor] with No[Util]
}

That's because IIUC the paper treats Excluded and Captured as lists, and simply filter elements of excluded to prevent them from appearing literally in Captured:

Excluded(res.type) = {T ∈ Excluded(s1.type) ∪ Excluded(s2.type) | T \not\in
Captured(s1.type), Captured(s2.type)}

(same with the formal type rules T-EComp).

I've wondered whether the use of \not\in actually checks not the set of types specified, but the set of all subtypes of Captured, which would fix the problem. However, that interpretation would apply also to Excluded, and it's not clear how to recover a minimal list of types. Moreover, rule T-ESpore explicitly uses <: to prevent similar problems, while I find no mention of the issue I describe.

It also seems a fix for this case might be simple:

Excluded(res.type) = {T ∈ Excluded(s1.type) ∪ Excluded(s2.type) | \not\exist U \in
Captured(s1.type), Captured(s2.type) (U <: T)}

but I haven't even began to look at the proof to check if it works.