I’m having troubles with understanding pattern matching on dependent types. Let’s say we have following code:

Variant Op := op1 | op2.

Variant Res : Op -> Set :=
| r1 : Res op1
| r2 : Res op2
| rb : forall op, Res op
.

Variant Node := n1 | n2.

Definition nops (n: Node) : Op :=
  match n with
  | n1 => op1
  | n2 => op2
  end.

Definition nedg (n: Node) (rv: Res (nops n)) : bool :=
  match n, rv with
  | n1, r1 => true
  | n1, rb _ => false
  | n2, r2 => true
  | n2, rb _ => false
  end.

As it is written, it curses about non exhaustive pattern-matching in nedg, because we do not consider n1, r2 and n2, r1 branches. Given nedg declaration, our moral right to cut them away is pretty obvious, so, the question is, what would be the most idiomatic way to convince type checker that omitted branches are actually impossible?