with syntax on records restricts return types unnecessarily

[mjp41]

with syntax for records does not allow the polymorphic type to be different between the
original and new record.

Repro steps

type Record<'a> = { plain : int; poly : 'a }

let update1 (f : 'a -> 'b) (r : Record<'a>) : Record<'b> =
    { r with poly = f r.poly }

Expected behavior

Typing update1 with the specified type. I always considered with on records
as shorthand for expanding the record creation, but the typing does not treat
them like that.

Actual behavior

The update1 the 'b and 'a are unified unnecessarily.

Known workarounds

Expanding the with to write the whole underlying record directly.

let update2 (f : 'a -> 'b) (r : Record<'a>) : Record<'b> =
    { plain = r.plain; poly = f r.poly }

Related information

This is on Visual Studio 2015 Update 2.

I am happy to fix this, but I can't currently work out if inferring a more general type
would potentially break existing code. Are there any corner cases where principle
typing does not work for F#?

[dsyme]

...but I can't currently work out if inferring a more general type
would potentially break existing code.

Presumably examples that involve the value restriction would hit this?

[dsyme]

I can't specifically remember any reason for this restriction.

It would be good to check if this is a design change (according to the F# language spec).

[mjp41]

@dsyme, it would require the language spec to change.

    The expression [left hand side of the with] is first checked with 
    the same initial type as the overall expression. 

You are correct the value restriction would bite here:

let update3 = 
   ref (fun f (r : Record<int>) -> { r with poly = f r.poly })

let update4 =
   ref (fun f (r : Record<int>) -> { plain = r.plain; poly = f r.poly })

At the moment, update3 type checks and update4 does not. But the change to make update1 type checks would make update3 not type check.

[dsyme]

Chatted with @mjp41 and we decided to close this since it would be a breaking change (due to the calue restriction).