Semantic lemmas for Scala 2 type projections T#A.

This shows how to restrict type projections to be sound and usable in Dotty. This is developed as an extension of guarded DOT (gDOT), described in the ICFP'20 paper "Scala Step-by-Step". (Homepage: https://dot-iris.github.io ). Because of the interest to the wider Scala community, this file has extensive informal comments. The comments use a "naive" understanding of types as sets; this Coq development is based on this understanding, but with some restrictions discussed in the paper.

Semantic proofs of typing lemmas for existentials.

I adapted the rules from https://dl.acm.org/doi/pdf/10.1145/3290322 (see ≤∃L and ≤∃R in Fig. 4). Lionel Parreaux pointed me to that paper and suggested they are the "standard" rules for "implicit" existentials.

Rule ∃-<: (called ≤∃L in the link).

Rule <:-∃ (called ≤∃L in the link).

Semantics of type projections.

This semantic type models upper-bound-only type projections using (model-level) existentials and normal DOT type members: V[[T#A]](ρ) = { v | ∃ w ∈ V[[T]](ρ). v ∈ V[[w.A]](ρ) }.

Technical infrastructure for setoid rewriting.

Semantic proofs of typing lemmas for projections.

Existentials on a singleton coincide with path substitution: ∃ x: p.type. T = T[x:=p].

Projections from a singleton coincide with selections: p.type#A = p.A.

TODO: other rules should be derivable from the rules for existentials. Here and below, we use indexed subtyping Γ ⊨ T <:^i U to satisfy the restrictions discussed above. These restrictions are not specific to type projections but are also needed for type selections p.A. On a first read, you should read Γ ⊨ T <:^i U as Γ ⊢ T <: U; see the paper for more discussion. In short, to show a subtyping relation T1 <: T2, we must show that any value v in T1 is also in T2. Because types can contain free variables, we have environments ρ, typed by typing contexts Γ, but you can ignore them at first. Type projections are covariant: if T <: U then TA <: UA, or formally: Γ ⊨ T <:^i U

---

Γ ⊨ T#A <:^i U#A

From T <: U we must show T#A <: U#A, that is, that any v in T#A is in U#A. Recall the definition of T#A: V[[T#A]](ρ) = { v | ∃ w ∈ V[[T]](ρ). v ∈ V[[w.A]](ρ) }. So assume v is in T#A; then there exists a w in T such that v is in w.A. But then w is in U, because T <: U. So we have w ∈ U and v ∈ w.A, that is, v ∈ U#A.

Type projections are subtypes of their upper bound.

---

Γ ⊨ { A :: L .. U }T#A <:^i U

Type projections are subtypes of their upper bound: a more general statement. Γ ⊨ T <:^i { A :: L .. U }

---

Γ ⊨ T#A <:^i U

Projections T#A are lower bounded by type selections p.A: Γ ⊨ p :^i T

---

Γ ⊨ p.A <:^i T#A Derive this rule from the above ones: rewrite the selection as a projection from a singleton type, then use covariance of projections, and finally use sSngl_Stp_Self to show that p.type <: T.

Combining the two above rules for projections with the existing system, we even get lower bounds for projections from inhabited types: Γ ⊨ T <:^i { A :: L .. U } Γ ⊨ p :^i T

---

Γ ⊨ L <:^i T#A But this is not the Scala 2 lower-bound rule (which doesn't require p to exist), and it is not directly usable for a typechecker. The only typing rule we can use in Scala is sSel_Stp_Proj, and to use that the user needs to get a value of type p.A in the usual, safe way: if e has type L, then e : p.A has types p.A and T#A. However, a typechecker might relax this restriction if it can prove T has an inhabiting path (that is, that it is realizable, in the sense used in Dotty), even if the value has not been constructed. Such reasoning is needed to enable compiling: trait T { type A = Int }; def f(x: Int): T#A = x. The value can even use assumptions in the typing context (which might be more liberal than the Dotty rules); as usual, code in absurd typing contexts cannot run.

In fact, if p has more specific bounds, we can use those too.

And sProj_Stp_L is indeed a special case of sProj_Stp_L_Gen.

TODO: Scala probably has more typing rules. Check them, or provide counterexamples.

Rules for projecting members with matching bounds.

Upper bounds are easy...

For lower bounds, we'd expect a rule similar to: Γ ⊨ T <:^i { A :: T .. T }#A However, we must first of all "guard" it with ▷, like other gDOT rules involving (g)DOT's impredicative type members; that would give: Γ ⊨ ▷ T <:^i { A >: T <: T }#A where { A >: T <: T } means { A :: ▷ T .. ▷ T }. In our notation, that's written: Γ s⊨ oLater T <:[i] oProj A (oTMemL A T T). That rule indeed holds, but was challenging to prove, because this rule involves a type definition that doesn't appear in the source program, and the setup described in our ICFP'20 paper does not support such type definitions for technical reasons. Luckily, we only needed to tweak our model a bit, preserving all results. Technically, in Iris jargon, to enable this proof we prepended a basic update modality (|==>) to the definitions of all semantic judgments, to allow using oProj_oTMem despite its own update modality. Luckily, it was easy enough to update the proofs for these changes in definitions; see: https://github.com/Blaisorblade/dot-iris/pull/303 .

Auxiliary lemma.

To prove this theorem, we create an auxiliary definition body auxD and an auxiliary object auxV, whose type member A points to shift T.