[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request for feedback

[Dan Licata]

> 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