For those interested, I recently have been thinking of a better way to specify type inference with principal derivations that lends itself better for type system extensions:
https://www.microsoft.com/en-us/research/uploads/prod/2024/0...
Still a bit preliminary but hopefully fun to read :-)
(I'll check out the new paper later - thank you for the link)
About duplicate labels.. one needs to retain the duplicate field at runtime _if_ there is a "remove_l" or "mask_l" operation that drops a field "l". For example, `{x=2,x=True}.remove_x.x` == `True`. (Where the type of `remove_l` is `{l:a|r} -> {r}`)
This comes up with effect systems where we could have 2 exception handlers in scope, and the current effect would be `<exn,exn>` (which corresponds to a runtime evidence vector `evn` of `[exn:h1,exn:h2]` where the h1,h2 point to the runtime exception handlers.). If a user raises an exception it'll select `evn.exn` and raise to `h1`. But a user can also "mask" the inner exception handler and raise directly to `h2` as well as `evn.mask_exn.exn`.
One could design a system though with different primitives and not have a remove or mask operation, such that the duplicate fields do not have to be retained at runtime (I think).
(Anyway, feel free to contact me if you'll like to discuss this more)