[Haskell-cafe] Cannot update a field in a record with a polymorphic type.

[Olaf Klinke]

I take it that in the expression

(defaultY ∷ ∀ α. Monoid α ⇒ Y α) {y = "c"}

the compiler is not smart enough to infer that the concrete value of α
is irrelevant for the outcome and therefore rejects the program. The
obligation here is to prove that the function

λ x. x {y = "c"} :: ∀ α. Y α -> Y String

is constant across all possible values of α, which I guess is
undecidable for general one-parameter types? Or is there a free theorem
saying that whenever a function has this general type signature, then
the α cannot possibly be used? This certainly fails if Y has more type
parameters that remain constant in the expression: A type class could
distinguish the extra type parameters even if at the value level the
result is constant across all α.

Olaf