List.chop throws an exception when a recursive call is missing a parameter

[agrn]

Hi,

When a recursive call in an equation is missing a parameter:

From Equations Require Import Equations.
Require Import List Nat.

Variant operation :=
  | do_first
  | do_second.

Definition measure op :=
  match op with
  | do_first => 1
  | do_second => 0
  end.

Definition measure_rel := Program.Wf.MR lt measure.

#[local] Instance wf_measure_rel : WellFounded measure_rel.
Proof.
  red.
  apply Wf.measure_wf, Wf_nat.lt_wf.
Qed.

Equations crash (op : operation) (l : list nat) : bool by wf op measure_rel :=
  (* First step *)
  crash do_first l => crash do_second;

  (* Second step *)
  crash do_second l => true.

List.chop will throw an exception:

File "./equations_bug_test.v", line 22, characters 0-186:
Error: Anomaly "Uncaught exception Failure("List.chop")."
Please report at http://coq.inria.fr/bugs/.

Full stack trace, made with OCAMLRUNPARAM=b coqc equations_bug_test.v:

File "./equations_bug_test.v", line 22, characters 0-186:
Error: Anomaly "Uncaught exception Failure("List.chop")."
Please report at http://coq.inria.fr/bugs/.
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Covering.add_wfrec_implicits.aux.(fun) in file "src/covering.ml", line 336, characters 40-70
Called from Covering.interp_constr_evars_impls in file "src/covering.ml", line 345, characters 10-45
Called from Covering.interp_glob_constr_evars_impls in file "src/covering.ml" (inlined), line 352, characters 22-78
Called from Covering.interp_program_body in file "src/covering.ml", line 365, characters 4-69
Called from Notationextern.with_notation_uninterpretation_protection in file "interp/notationextern.ml", line 188, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Notation.with_notation_protection in file "interp/notation.ml", line 2571, characters 14-59
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Pcoq.with_grammar_rule_protection in file "parsing/pcoq.ml", line 490, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Metasyntax.with_lib_stk_protection in file "vernac/metasyntax.ml", line 1528, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Covering.interp_constr_in_rhs_env in file "src/covering.ml", line 417, characters 19-71
Called from Covering.interp_clause in file "src/covering.ml", line 1324, characters 6-121
Called from Covering.covering_aux in file "src/covering.ml", line 1165, characters 12-133
Called from Covering.covering_aux.try_split.coverrec in file "src/covering.ml", line 1199, characters 15-278
Called from CArray.fold_left_map.(fun) in file "clib/cArray.ml", line 435, characters 43-50
Called from Stdlib__Array.map in file "array.ml", line 106, characters 21-40
Called from CArray.fold_left_map in file "clib/cArray.ml", line 435, characters 11-67
Called from Covering.covering_aux.try_split in file "src/covering.ml", line 1217, characters 36-92
Called from Covering.covering_aux in file "src/covering.ml", line 1239, characters 20-41
Called from Covering.covering.(fun) in file "src/covering.ml", line 1606, characters 8-72
Called from Covering.program_covering in file "src/covering.ml", line 1622, characters 4-69
Called from CList.map2 in file "clib/cList.ml", line 313, characters 21-26
Called from Covering.coverings in file "src/covering.ml", line 1626, characters 19-79
Called from Equations.define_by_eqs in file "src/equations.ml", line 164, characters 17-69
Called from Equations.equations in file "src/equations.ml", line 214, characters 4-79
Called from Vernacextend.vtmodifyprogram.(fun) in file "vernac/vernacextend.ml", line 180, characters 29-34
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 133, characters 2-59
Called from Ccompile.compile_file in file "toplevel/ccompile.ml", line 142, 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

I use Coq 8.17.1 and Equations 1.3 from opam.

% coqc --version
The Coq Proof Assistant, version 8.17.1
compiled with OCaml 4.14.1

Of course, replacing crash do_second by crash do_second l works.