Adam Welc

> > neither $t0 nor $t1 in mid is a vector type: $t0|has_vector: &mut m1::HasVector and $t1: &mut m1::HasAnotherVector > > Right, but `$t0` has a field `v` that is...

> Have you debug print the `dst_ty` in the `match dest_ty` which causes the issue (sorry if I missed it)? I have but did not include it as it's not...

> I wonder what the priority of this (clear) bug is. Is this important for you? If so do you not have a reasonable workaround? The minimal example was distilled...

I dug a little deeper for learning purposes but also since I want this out of the way. The comment for [`summarize` function](https://github.com/move-language/move/blob/c9bce5832193fef28dfd680b6f91c5ced15e0ff2/language/move-prover/bytecode/src/borrow_analysis.rs#L225) in borrow analyzer says the following: ```...

> I think the later sub-edges are taken into consideration too. `translate_write_back_update` is a recursive function. Right... This is some complicated code! To continue the analysis, though, if we have...

I think I finally figured out where the bug is after running the algorithm through some examples on paper. I will try to put together a PR tomorrow to see...

@wrwg, @emmazzz - I have created a PR where I attempted to fix the problem: https://github.com/move-language/move/pull/289 (please PR's description for details).

I am not sure if the idea being currently explored involves (somehow) re-using the existing formatter or writing one from scratch, but here's a general idea of what would be...

I am not sure if starting with the existing formatter is the best idea. Not only using "official" Move parser would result in a different AST which would require modifying...

> comments which need to be preserved (this excludes e.g. using the current parser, which throws comments away even before the lexer is run) Indeed, existing parser would have to...