Mechanized type inference for record concatenation

This is quite a detailed post, and I appreciate the clear motivation behind the data structures and the new notations!

However, PL is an intersection between mathematics and human factors, and for this example,

>>> r: s: ((r without x) // (s without x)).x + 1
Field mismatch

the error message being just "Field mismatch" is somewhat concerning. I would expect the algorithm to support both checking the types and providing detailed messages that can help understand the cause of the error (even if the user doesn't know how the constraint system works). I assume that adding tracking to explain the chain of constraints that lead to the error would affect the algorithm? Or is doing so roughly trivial and just not the point of the post? (If so, I'd love to know what the errors look like for this and other examples with tracking added)

I wonder how helpful/related Cue's notion of the lattice is to this problem of late-binding type-checking.