Me:

...

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.

Dan:

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?

There are two components to this process, and they're quite separable. Let's have an example (in fantasy dependent Haskell), for safe lookup. defined :: Key -> [(Key, Val)] -> Bool defined k [] = False defined k ((k', _) : kvs) = k == k' || defined k kvs data Check :: Bool -> * where OK :: Check True lookup :: (k :: Key; kvs :: [(Key, Val)]) -> Check (defined k kvs) -> Val lookup k [] !! -- !! refutes Check False; no rhs {-before-} lookup k ((k', v) : kvs) p with k == k' {-after-} lookup k ((k', v) : kvs) OK | True = v lookup k ((k', v) : kvs) p' | False = lookup k kvs p' Left-hand sides must refine a 'problem', initially lookup k kvs p where k :: Key; kvs :: [(Key, Value)]; p :: Check (defined k kvs) Now, {-before-} the with, we have patterns refining the problem lookup k ((k', v) : kvs) p where k, k' :: Key v :: Val kvs :: [(Key, Val)] p :: Check (k == k' || defined k kvs) The job of "with" is only to generate the problem which the lines in its block must refine. We introduce a new variable, abstracting all occurrences of the scrutinee. In this case, we get the new problem {-after-}. lookup k ((k', v) : kvs) p | b where k, k' :: Key v :: Val kvs :: [(Key, Val)] b :: Bool p :: Check (b || defined k kvs) All that's happened is the abstraction of (k == k'): no matching, no mucking about with eliminators and motives. Now, when it comes to checking the following lines, we're doing the same job to check dependent patterns (translating to dependent case analysis, with whatever machinery is necessary) refining the new problem. Now, once b is matched with True or False, the type of p computes to something useful. So there's no real guesswork here. Yes, it's true that the choice to abstract all occurrences of the scrutinee is arbitrary, but "all or nothing" are the only options which make sense without a more explicit mechanism to pick the occurrences you want. Such a mechanism is readily conceivable: at worst, you just introduce a helper function with an argument for the value of the scrutinee and write its type explicitly. I guess it's a bit weird having more structure to the left-hand side. The approach here is to allow the shifting of the problem, rather than to extend the language of patterns. It's a much better fit to our needs. Would it also suit Haskell? Cheers Conor