Error: Anomaly "Uncaught exception Option.IsNone." Please report at http://coq.inria.fr/bugs/. with recursive notations

[JasonGross]

Description of the problem

Axiom Reduction_sum : forall {A}, nat -> nat -> nat -> (nat -> A) -> A.
#[local] Notation "'einsum_partλ0' s => body"
  := (fun s => Reduction_sum 0 s 1 (fun s => body))
       (at level 200, s binder, only parsing).
#[local] Notation "'einsum_partλ' s1 .. sn => body"
  := (einsum_partλ0 s1 => .. (einsum_partλ0 sn => body) .. )
       (at level 200, s1 binder, sn binder, only parsing).
(*
Error: Anomaly "Uncaught exception Option.IsNone."
Please report at http://coq.inria.fr/bugs/.
*)

Backtrace

Raised at Option.get in file "clib/option.ml" (inlined), line 50, characters 9-21
Called from Notation_ops.compare_recursive_parts in file "interp/notation_ops.ml", line 589, characters 36-60
Called from Notation_ops.notation_constr_and_vars_of_glob_constr.aux in file "interp/notation_ops.ml", line 600, characters 8-82
Called from Notation_ops.notation_constr_and_vars_of_glob_constr in file "interp/notation_ops.ml", line 665, characters 10-15
Called from Notation_ops.notation_constr_of_glob_constr in file "interp/notation_ops.ml", line 718, characters 27-76
Called from Constrintern.interp_notation_constr in file "interp/constrintern.ml", line 2678, characters 22-59
Called from Metasyntax.make_notation_interpretation in file "vernac/metasyntax.ml", line 1695, characters 36-76
Called from Metasyntax.add_notation in file "vernac/metasyntax.ml", line 1798, characters 17-108
Called from Vernacextend.vtdefault.(fun) in file "vernac/vernacextend.ml", line 125, characters 29-33
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 Stm.finish in file "stm/stm.ml", line 2423, characters 12-50
Called from Stm.process_transaction in file "stm/stm.ml", line 2690, characters 22-45
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.add in file "stm/stm.ml", line 2788, characters 8-50
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 61, characters 28-90
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

coq/interp/notation_ops.ml

Line 589 in 99f5ecc

NBinderList (x,y,iterator,f (Option.get !terminator),revert)

cc @herbelin ?

Coq Version

8.17.0

[herbelin]

By chance, I saw this bug while providing PR #17856 (w/o taking time to find an example though). So, this is fixed by commit 6ebf4e5 there.

Since 8.18 is approaching and I'm not sure that #17856 can go in, I made also a specific PR #17861.