Fix typing rules for paths about dot-iris HOT 3 CLOSED

Avoiding updates appears to matter in a few places (I gave a quick try some time ago) [...] We might be able to add updates by adding them to value subtyping as well, but I'm pretty wary of the idea — I'm not certain it'd work.

Thinking about this again. Of course, that'd be later update. Or maybe the future modality (n (later update) + 1 update?). EDIT: the same would happen in TLater's semantics...

from dot-iris.

I have not tried proving typing lemmas for paths of arbitrary length, but the ones I did try (for length = 2) followed my expectations.

Just sketched the proofs on paper, I’ll need to change the typing rules quite a bit, and quite possibly simplify the definition of path_wp. The impact here seems not too worrisome, tho the rules look pretty different. They’re equivalent to the ones on paper when p :^i T and length p = i, but they’re different when length p < i.

from dot-iris.

This is the last part missing for the fundamental lemma, after #11 is fixed by #42.

from dot-iris.