
I wrote:
Yes. The translation of record updates given in the Report makes perfect sense for {}. It is only forbidden by "n >= 1", but no reason is given for that restriction.
d wagner wrote:
It doesn't make sense to me. The translation explodes a value into a case statement over its constructors; what constructors do you use when you don't know the type of the value? When n >= 1, you know the type of the value by looking where the field came from, and hence which constructors to use in the case statement.
Well, yes, you need to know the type. That's why I asked Simon if there is difficulty with implementation. I do have an algorithm in mind, but it seemed silly for me to write it out given that I know near zero about the implementation details of GHC's type checker. But if you insist, here is a rough sketch: Replace each subexpression of the form e {} by v' and add v = e to the let bindings, where v and v' are fresh variables. Resolve the type. For any v that resolves to an ADT (even if the types of its parameters are not resolved), replace e {} in the original expression by its case expansion. Repeat until all are resolved, rejecting the program if an iteration does not resolve any v. Resolve the final form of the expression one more time to obtain its type. Does this make any sense? Thanks, Yitz