Lambda the Ultimate

I spent bit of time recently reading up on BETA and gbeta, and I've run into a question that I haven't seen answered. I'm not sure if this is appropriate to LtU, but I honestly can't think of many other places where I could ask this and expect a meaningful/accurate response.

In BETA, when I extend or further-bind a pattern, I can add new part object declarations, as well as add to the "enter," "exit," and "do" parts. The thing is, wouldn't adding to the "enter" part mess with subtyping/covariance? Cast in more common OOP terminolgy, this would be like allowing a programmer to override an inherited virtual method and add additional parameters!

Do BETA/gbeta make this a run-time error? Do they just leave variables uninitialized in cases where not enough values are provided as input to a pattern? I haven't seen any statements on this point.

In Spark I had to put a bit of thought/effort into resolving this issue, so I wouldn't be surprised if there were prior work I just wasn't aware of.