Record typing question

[William Chesters <williamc@dai.ed.ac.uk>]

Spooky, I raised this point a few days ago!

There is a slight complication, because of cases like

    type 'a foo = { a: 'a; b: 'a }
    let f x = { x with a = 1 }

    let _ = f { a: "one"; b: "one" }

Here "f: 'a foo -> int foo" won't wash, because the "b" field will
stay an int, contra the definition.  Before lifting the current
restriction, one would have to check that no type equalities between
fields are broken.

Nevertheless, I don't see a problem in principle and it would be good
to see a more general version.

Don Syme writes:
 > 
 > The typing rule for record overriding seems slightly more restrictive than
 > necessary, though I can imagine this is because it was simplest to implement
 > it this way.  e.g.
 > 
 > # type 'a foo = { a: 'a; b: int };;
 > type 'a foo = { a: 'a; b:int }
 > # let f x = {x with a=1 };;
 > val f : int foo -> int foo = <fun>
 > 
 > Why doesn't f have type 'a foo -> int foo??