Coincidentally, I've been thinking about (a small part of) this issue for a day or two. I think it would probably be pretty easy to add a language feature that basically brought what the compiler does up to the Haskell level. Imagine a sort of *generalized* as-pattern:
f x@@(Right y) = ...
`x` here is not bound to the actual argument; instead, it is bound to `Right y`. The type of `x` will either be inferred or given explicitly:
f (x :: ...)@@(Right y) = ...
How can this translate to Core? Roughly speaking, it would look like
f _x = case _x of
Left p -> ...
Right y ->
let x = unsafeCoerce _x
in ...
But `x` would be given the unfolding `Right y`.
For existentials and GADTs, the type checking and Core translation needs some extras. In particular, the dictionary arguments need to be included to ensure the coercion is valid. Just make sure they match. The special ~ and Coercible constraints don't need to be included in that check, but it must be possible to produce coercions with the appropriate types.