In the semantics that I have in mind, p and (e with q) only matches values that match p and for which the value of e (which may use variables from e matches q), so your with p = e is entirely subsumed by the and e with p. You can write Some y | None and (0 with y). I agree that it doesn’t read as nicely as with y = 0 for this specific usage, but it extends better to the more complex usages (in particular, for view patterns, it respect the natural ordering of the function-part and the pattern-part, even in absence of the syntactic sugar).