Thanks for the further explanation, Marcin. If I understand correctly, you're talking about explicitly named algebraic types, not just unions where the type is an anonymous reflection of the structure as in: Var (foo :: Int, bar :: Char) -- in the style of "A Polymorphic Type System for Extensible -- Records and Variants" (Gaster & Jones) and: Either Int (Either Char ()) -- in the extensible union type mechanism of "Monad Transformers -- and Modular Interpreters" (Liang, Hudak & Jones) I've sometimes wondered whether it would be appropriate to implement the summing aspect of `data' by wrapping `newtype' around such extensible variants. (There'd still need to be some construct for the other aspects of `data': products and strictness flags.) For example, this: data T a b = T1 a !Int | T2 b could translate to something like this: newtype T a b = T {unT :: Var (t1 :: (a, !Int), t2 :: b)} Then there'd be a way to extract a value of a structurally named type from a value of an explicitly named type. Would this help to combine explicitly named types with add-a-field subtyping and remove-a-summand subtyping? For that matter, is it how O'Hugs already works beneath the surface? Regards, Tom