I don’t think it’s exactly the same as in Daan’s paper.
For example, every record literal has concrete type. So { x = "hi" } can never have a type like { a | x : String } which is really important for getting good error messages in case expressions.
In contrast, I believe @X "hi" would need to have the open type [a | @X String ] if you wanted to try to make it like record types. I believe this is the only way way it could be fed into a case expressions expecting a closed [ @X String or @Y Int ] type with rules similar to Daan’s. I think that’s an important difference when it comes to error message quality!
And if the literal type is open, wouldn’t the whole case result type be open too? Or is there a special typing rule for case expressions that does not appear in Daan’s paper?
I think these kinds of differences would come out in typing rules specific to your idea.
Note: I included the OCaml quote for readers who may be new to this topic. I personally cannot fully evaluate how a proposal like this differs other things without seeing the specific typing rules.