Extensible downcasts impossible in Haskell?

[Tom Pledger]

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