Record spread that copies a mutable field is generalized (unsound) #9156

A record literal with a spread, {...base, field: value}, has its type generalized even when it copies a mutable field from base. The literal allocates a fresh record with that mutable field, so one binding can be written at one type and read at another:

type cell<'a> = {tag: int, mutable value: option<'a>}

@val external base: cell<'a> = "base"

let copy = {...base, tag: 1}
copy.value = Some(1)
let s: option<string> = copy.value

This compiles on master (8e26a9c) and generates:

let init = base;
let copy = {
  tag: 1,
  value: init.value
};
copy.value = 1;
let s = copy.value;

so s, typed option<string>, holds the number 1. The same happens with optional mutable fields ({tag?: int, mutable value?: 'a}).

Cause

The value restriction (Typecore.is_nonexpansive) checks a spread literal's written fields for mutability and requires the spread expression to be non-expansive, but treats the fields it copies from the spread as harmless. A spread literal allocates every field of the record, so a mutable field makes it expansive whether it is written or copied, just like a literal without a spread (#9149, #9152).

base has to be a polymorphic, non-expansive value of a record type with a mutable field. A record literal of such a type is itself expansive, so in practice base is an external, for example a binding to a default options object: @val external defaults: options<'a> followed by {...defaults, x: 1}.