Moc currently accepts:
let x : { var v : Int } = {
var v : Nat = 1;
};
and correctly rejects:
let x : { var v : Nat } = {
var v : Nat = 1;
};
let y : { var v : Int } = x;
The former is dubious, but I can't actually get it to go wrong because there is no way to alias the field v at both types.
Morally, this example would demonstrate unsoundness:
let x : { var v : Int; var w : Nat} = {
var v : Nat = 1;
alias w = v
};
Since x.v := -1 would (also) assign -1 to x.w, a Nat.
But I don't see how to emulate this, so perhaps we are safe after all.