#[tactic=tac] should apply to omitted cases

[yforster]

Definition inverts {X} {Y} (g : X -> Y) (f : Y -> X) := forall x, g (f x) = x.

From Equations Require Import Equations.

Definition inspect {X} (x : X) : {y | x = y}.
  now exists x.
Defined.
Notation "a eqn: E" := (exist _ a E) (at level 40).

#[tactic=congruence]
Equations R {X} {Y} (f : option X -> option Y) g (H : inverts g f) (x : X) : Y :=
  R f g H x with (inspect (f (Some x), f None)) :=
    R f g H x ((Some y, _) eqn: E1) := y ;
| (None, Some y) eqn:E := y ;
.

gives me

Error:
Non-exhaustive pattern-matching, no clause found for:
R X Y f g H x ((None, None) eqn: e)
In context: 

X : Type
Y : Type
f : option X -> option Y
g : option Y -> option X
H : inverts g f
x : X
e : (fun y : option Y * option Y => (f (Some x), f None) = y) (None, None)

although inserting | (_ , _) eqn: E := _ or more explicitly | (_ , _) eqn: E := ltac:(congruence) works.

I would have expected that for non-exhaustive pattern matchings, the tactic specified via the attribute is used to derive a contradiction if possible. Apparently that's not how it works, but I'd like that as a feature!

[mattam82]

That sounds slightly dangerous, how about #[missing=tactic] or something similar? @TheoWinterhalter do you have this use case as well?

[TheoWinterhalter]

I don't have this use-case, I usually prefer to be explicit about matched cases that aren't necessary.

[yforster]

#[missing=tactic] would be similarly fine for me