I agree with Ben. I generally expect not to see nested casts -- the Cast constructor should rarely (never?) appear as an expression outside of mkCast. But you're right about the missing optimization opportunity if we do the naive thing.
Let us know if you run into trouble with the "quick try"!