# Is it a good idea to modify the context during type checking of patterns?

So I'm working on type checking of an expression that pattern matches on terms, like case x of in Haskell. My question is, suppose we have case x of { X => ? } where:

1. x is a variable
2. X is a pattern
3. There are other variables in the context whose type uses x

When we are at ?, should we replace x in the types from the context with X? In other words, should pattern matching expression update the context?

I have the impression that Agda does this, but this does not scale to arbitrary expressions (being matched), like a function call. Is it a good idea to keep the context as-is? If so, what is the recommended approach to update the context, given that the user really wants to do so?

• Does agda even have case expressions? I thought they are emulated by clausal definitions plus function applications.
– Trebor
Oct 27 at 14:08
• Yes, Agda sugarize these things, but is it a good idea? Oct 27 at 22:51

There are multiple patterns you can use to emulate your feature, that mainly work by interleaving the case in the middle of a β- or ι-redex (what I have heard called a "commutative cut", I think the name comes from the linear logic literature). A simple one is to abstract over the context variables you want to make more precise: if the context is say x : nat, v : Vect bool x, you can build case x of { 0 => fun (v' : Vect bool 0) => … | S n => fun (v' : Vect bool (S n) => …} v. In each branch v' can be used instead of v, with its type properly refined. Note that this is not specific to v being a variable in the context, it can really be any term whose type you want to refine. In particular, you can do the following: case x of {p => fun (e : x = p) => …} eq_refl and in the branch use e to showcase the fact that x has been refined. This is usually called the convoy pattern, name coined in Chlipala's Certified Programming with Dependent Types. Note that both these approaches work even in the scrutinee is not a variable.