Error: Anomaly "Uncaught exception Failure("hd")." Please report at http://coq.inria.fr/bugs/. with overlapping names in Constrintern.check_or_pat_variables

[JasonGross]

Description of the problem

From Coq Require Import Qround Sint63 Uint63 NArith PArith ZArith QArith Floats.
Local Open Scope float_scope.
Notation "'∞'" := infinity : float_scope.
Check let j := 5 in
        match Prim2SF j, Prim2SF (-j) with (* inl i or inr return *)
        | S754_nan, _ => inr nan
        | S754_zero _, _ => inl 0%Z
        | S754_infinity false, _ => inr ∞
        | S754_infinity true, _ => inr (-∞)
        | S754_finite false m e, _
          => inl (_ (e - shift)%Z)
        | S754_finite true m e, S754_finite false m e
        | S754_finite true m e, _ => inr nan (* should be impossible *)
        end.
(* Error: Anomaly "Uncaught exception Failure("hd")."
Please report at http://coq.inria.fr/bugs/.
 *)

According to the backtrace, the use of floats is probably not relevant, cc @herbelin for deep pattern matching issues?

Backtrace (from Compute rather than Check)

Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Stdlib__list.hd in file "list.ml" (inlined), line 30, characters 10-23
Called from Constrintern.check_or_pat_variables in file "interp/constrintern.ml", line 1475, characters 16-31
Called from Constrintern.internalize.intern_disjunctive_multiple_pattern in file "interp/constrintern.ml", line 2361, characters 4-49
Called from Constrintern.internalize.intern_eqn in file "interp/constrintern.ml", line 2366, characters 22-71
Called from CList.map_loop in file "clib/cList.ml", line 291, characters 21-24
Called from CList.map in file "clib/cList.ml", line 299, characters 4-18
Called from Constrintern.internalize.intern.(fun) in file "interp/constrintern.ml", line 2250, characters 20-68
Called from Constrintern.internalize.intern.(fun) in file "interp/constrintern.ml", line 2132, characters 10-91
Called from Constrintern.intern_unknown_if_term_or_type in file "interp/constrintern.ml" (inlined), line 2564, characters 2-29
Called from Vernacentries.vernac_check_may_eval in file "vernac/vernacentries.ml", line 2012, characters 11-67
Called from Vernacentries.translate_vernac.(fun) in file "vernac/vernacentries.ml", line 2568, characters 8-43
Called from Vernacextend.vtreadproofopt.(fun) in file "vernac/vernacextend.ml", line 159, characters 29-44
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 207, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 257, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 255, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2173, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 960, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2315, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2412, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Flags.silently in file "lib/flags.ml" (inlined), line 64, characters 19-40
Called from Vernac.load_vernac_core.loop in file "toplevel/vernac.ml", line 120, characters 8-69
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 124, characters 6-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.load_vernac in file "toplevel/vernac.ml", line 180, characters 30-94
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 64, characters 18-95
Called from Ccompile.compile in file "toplevel/ccompile.ml" (inlined), line 132, characters 2-59
Called from Ccompile.compile_file in file "toplevel/ccompile.ml", line 141, characters 4-61
Called from Coqc.coqc_main in file "toplevel/coqc.ml", line 48, characters 2-100
Called from Coqc.coqc_run in file "toplevel/coqc.ml", line 67, characters 4-36

This is the error message in

coq/interp/constrintern.ml

Lines 1464 to 1475 in 99f5ecc

	let check_or_pat_variables loc ids idsl =
	let eq_id {v=id} {v=id'} = Id.equal id id' in
	(* Collect remaining patterns which do not have the same variables as the first pattern *)
	let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in
	match idsl with
	| ids'::_ ->
	(* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *)
	let ids'' = List.subtract eq_id ids ids' in
	let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in
	user_err ?loc
	(strbrk "The components of this disjunctive pattern must bind the same variables (" ++
	Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).")

so I'm guessing the problem is that this code is not robust to duplicated identifiers?

Coq Version

8.17.0

[JasonGross]

And, indeed, here's a smaller example:

Check fun b : bool
      => match b, b with
         | true as a, true as a
         | true as a, _
           => true
         | _, _ => false
         end.

[herbelin]

Thanks for the short example. The check for duplicate variables in a list of patterns and the check for a same set of bound variables in a disjunction of patterns were done in the wrong order, resulting in a wrong invariant for the second check. Fixed by PR #17857.