Why not allow empty record updates?

[Yitzchak Gale]

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