Overlapping structure sources should not be considered right-to-left

[Kha]

Consider the following structure updates:

structure A where
  an : Nat

structure B extends A where
  bn : Nat

def a : A := { an := 0 }
def b : B := { an := 1, bn := 1 }

example : { a, b with }.an = 0 := rfl
example : { b, a with }.an = 0 := rfl

The first example succeeds while the second one doesn't. I would have expected exactly the opposite and was very confused when that didn't happen.

[Kha]

This is likely working as expected; one should always prefer direct field access via to* if one cares about ordering, sharing, etc.