In the dependently typed setting, it's often the case that the "with-scrutinee" is an expression of interest precisely because it occurs in the *type* of the function being defined. Correspondingly, an Epigram implementation should (and the Agda 2 implementation now does) abstract occurrences of the expression from the type. That makes things a bit trickier to implement, but it's just the thing you need to replace "stuck" computations in types with actual values. The "with" construct is what makes it possible to keep all the layers of computation in step.
Oh, I see: you use 'with' as a heuristic for guessing the motive of the inductive family elim. How do you pick which occurrences of the with-scrutinee to refine, and which to leave as a reference to the original variable? You don't always want to refine all of them, do you? -Dan