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