[ssr] unclear view_subject / discharged_H is used in conclusion

[mrhaandi]

Description of the problem

Sometimes unexpectedly the ssreflect view mechanism fails with __view_subject__ is used in conclusion or __discharged_H__ is used in conclusion. Here is a small example (where the conclusion is False):

Require Import ssreflect.

Inductive zero : nat -> Prop := Z0 : zero 0.

Inductive is_zero0 : zero 0 -> Prop := is_zero0_intro : is_zero0 Z0.
Inductive no_zeroS (n : nat) : zero (S n) -> Prop :=.

Definition zero_inv {n} (e : zero n) :
  match n return zero n -> Prop with
  | 0 => is_zero0
  | S m => no_zeroS m
  end e.
Proof. by case: e. Defined.

Lemma test : zero 1 -> False.
Proof.
  Fail move=> /zero_inv.
  (* __view_subject__ is used in conclusion. *)
  move=> H.
  Fail move=> /zero_inv in H.
  (* __discharged_H__ is used in conclusion. *)
Abort.

Coq Version

The Coq Proof Assistant, version 8.18.0 compiled with OCaml 4.14.1

[silene]

While the error message is awful, the failure seems fine to me. When you apply the view zero_inv to the hypothesis __view_subject__: zero 1, the resulting term is no_zeroS 0 __view_subject__, thus preventing the removal of the hypothesis. This basically amounts to calling refine (fun H => _ (zero_inv H)).