Is there a complete list of terms `x`

such that `match x with _ => idtac end`

succeeds but `match x with x => idtac end`

fails? (I just discovered that any term containing unfolded primitive projections makes the cut, c.f. https://github.com/coq/coq/issues/15554)

how would we know if a list of bugs is complete?

I guess that's a good point, and I should have instead asked "does anyone know any other such terms?"

Well looking at the code, _ successes before x since it is obviously a wildcard. The later gets checked with

```
(** [pattern_match_term pat term lhs] returns the possible
matchings of [term] with the pattern [pat => lhs]. *)
let pattern_match_term pat term lhs =
match pat with
| Term p ->
begin
try
put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
return lhs
with Constr_matching.PatternMatchingFailure -> fail
end
| Subterm (id_ctxt,p) ->
let rec map s (e, info) =
{ stream = fun k ctx -> match IStream.peek s with
| IStream.Nil -> Proofview.tclZERO ~info e
| IStream.Cons ({ Constr_matching.m_sub ; m_ctx }, s) ->
let subst = adjust m_sub in
let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in
let terms = empty_term_subst in
let nctx = { subst ; context ; terms ; lhs = () } in
match merge ctx nctx with
| None -> (map s (e, info)).stream k ctx
| Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
}
in
map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error
```

Which is probably handling primitive records incorrectly.

@Jason Gross has anybody attempted to use something QuickCheck-like to test the relevant equality is reflexive?

@Paolo Giarrusso Not that I know of. Would it be hard to set up?

no idea, and I'm half-expecting there's too much mutable state in Coq terms for this

can `x`

be an Ltac-bound variable, or are you requiring it to be a copy-paste?

with evars you can probably do weird things courtesy of pattern_of_constr

@Pierre-Marie Pédrot I'd be interested in Ltac-bound variables too. I thought that pattern_of_constr sometimes turned specific evars into general holes, but for this to happen you need to get more restrictive.

Last updated: Oct 13 2024 at 01:02 UTC