Thank you Henning and Viktor. Indeed the update of the field goes through if its type is specified beforehand. But I am still not at peace. Consider: λ :type (defaultY ∷ ∀ α. Monoid α ⇒ Y α) {y = "c"} …Error… λ :type (defaultY ∷ Y ( )) {y = "c"} (defaultY ∷ Y ( )) {y = "c"} :: Y [Char] So, polymorphic types are not good enough to update. But see further: λ data Z α = Z {z₁, z₂ ∷ α} λ defaultZ = Z {z₁ = mempty, z₂ = mempty} λ :type (defaultZ ∷ ∀ α. Monoid α ⇒ Z α) {z₁ = "c"} (defaultZ ∷ ∀ α. Monoid α ⇒ Z α) {z₁ = "c"} :: Z [Char] — So when I have two fields it is suddenly fine to update a polymorphic field! I can infer that there is an invisible stage in the type checking process where all expressions must receive a final monomorphic type. I also understand that the surviving field `z₂` serves as a witness of the type `defaultZ` must have been specialized to: `"c" ∷ String` ⇒ `z₂ ∷ String` ⇒ `z₁ ∷ String`, and so type checking can succeed. But still, is this behaviour not obviously wrong? If a value of the transient instantiation of `defaultY` _(that exists only in the moment before its field is updated)_ is never observed, why does it need to be monomorphized? Why not be lazy about it?