Type safety and singletons
I am continuing to make progress on the proof of soundness for Featherweight Scala, but the most significant difficulty I am encountering involves the rule that allows paths, expressions of the form x.l1.l2...ln
, to be given singleton types:
Γ ⊦ p: T

Γ ⊦ p: p.type 
It seems to make any defining any sort of useful inversion principle impossible. For example, the term x.l1
where x
has a field val l1 : Int = 3
will reduce to 3
. In the proof of preservation, you would expect to be able to use inversion to show that if x.l1
is well typed with some type T
that x
has a field l1
with type T
, or at least some subtype of T
. However, with singletons it is possible that the type of x.l1
is x.l1.type
. In that case, the only thing you can determine by inversions is that x
has a field called l1
and it has some type. Many similar problems arise determining what would be seemingly straightforward facts because it is impossible to relate two types in a meaningful way.
There must be a resolution to the problem, because I know there are other type systems that allow singletons in this fashion, but I have not been able to hit upon the lemma to prove that will allow smoothing over the discontinuities singletons introduce. For now I think I will try proving safety with the above typing rule omitted, and see whether there are any other problematic features of the language.