Problem with Dependent pattern matching in COQ

Question

(small update to make it closer to my real task)

How to write f2 using dependent pattern matching? (Code below compiles except definition of f2)

Inductive parse_ret : Set :=
  No : parse_ret | Yes : parse_ret.

Inductive exp : parse_ret -> Set :=
| No_parse : exp No
| Yes_parse : exp Yes.

Definition f1 (p : parse_ret) : option (exp p) :=
  match p with
  | No => Some No_parse
  | Yes => Some Yes_parse
  end.
          
Definition f2' : option nat :=
  match f1 No with
  | Some No_parse => Some 1
  | Some Yes_parse => Some 1
  | None => None
  end.

So, f2' is almost what I need, but Some Yes_parse is obviously redundant here because we provided No constructor to f1 and f1's return type becomes option (exp No).

How to write definition for f2? avoiding the Non exhaustive pattern-matching error?

Definition f2 : option nat :=
  match f1 No with
  | Some No_parse => Some 1
  | None => None                            
  end.

Answer 1

This is, I believe, a defect of the pattern-matching compilation algorithm of Coq. This is the part that is responsible of elaborating a fancy pattern-matching you write as a user into one comprehensible by the kernel.

Here, it has to do two things: one is to desugar a deep pattern-matching (matching over option and exp at once) into two nested pattern-matching; the other is to detect that some constructors are not to be considered because of the typing constraint, which would allow you to avoid giving the Some Yes_parse clause. However, the algorithm is not able to do this in its current state.

Thus, you have to help it by hand. One possibility is to do part one for it, and write

Definition f2' : option nat :=
  match f1 No with
    | None => None
    | Some p =>
      match p in exp r with
        | No_parse => Some 1
      end
  end.

Coq is happy with this, and if you print the elaborated term you get

match f1 No with
| Some p =>
    match p in (exp r) return match r with
                              | No => option nat
                              | Yes => IDProp
                              end with
    | No_parse => Some 1
    | Yes_parse => idProp
    end
| None => None
end

where you see that the elaborator has massaged the inner match and introduced a smart return clause to handle the non-exhaustiveness issue.