Anomaly "in retype: Not an arity" when coercing from a structure to sig

[Tragicus]

In the following script, I have an element T of some structure S and I try to coerce an element x of T into @sig T P. The coercion search fails and asks coq-elpi to find a solution. elpi triggers unification between sort T and @sig ?e0 ?e2 and Coq raises an exception.

The code:

From elpi.apps Require Import coercion.

Elpi Accumulate coercion.db lp:{{

coercion Ctx V T E R :-
  std.spy (coq.unify-eq T {{ @sig lp:U lp:X }} ok),
  R = {{ @proj1_sig lp:U lp:X lp:V }}.

}}.
Elpi Typecheck coercion.

Structure S := Pack {
  sort :> Type;
}.

Canonical generic_S (T : Type) := Pack T.

Set Debug "unification".
Fail Check forall (T : S) (P : T -> Prop) (t : T) (x : @sig T P), x = t.

The debugging and error messages:

----<<---- enter:  
coq.unify-eq (app [global (const «sort»), c0]) 
 (app [global (indt «sig»), X0^4, X1^4]) ok

[unification] sort|ZApp(T)
              sig|ZApp(?e0, ?e2)

Anomaly "in retyping: Not an arity."

According to (https://github.com/coq/coq/issues/18252#issuecomment-1792555770), it looks like the error comes from coq-elpi adding evars ?e and ?e1 with ?e0 : ?e and ?e2 : ?e1 but not adding ?e := Type and ?e2 := Type.

[gares]

Please pass -bt to coqc and post the trace

[Tragicus]

Here it is:

Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Evarconv.conv_record.(fun) in file "pretyping/evarconv.ml", line 1190, characters 21-50
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Evarconv.conv_record in file "pretyping/evarconv.ml", line 1187, characters 6-533
Called from Evarconv.evar_eqappr_x.(fun).f3 in file "pretyping/evarconv.ml", line 1037, characters 18-77
Called from Evarconv.ise_try in file "pretyping/evarconv.ml", line 300, characters 12-18
Called from Evarconv.evar_conv_x.default in file "pretyping/evarconv.ml", line 587, characters 10-158
Called from Evarconv.unify in file "pretyping/evarconv.ml", line 1871, characters 12-51
Called from Coq_elpi_builtins.coq_builtins.(fun) in file "src/coq_elpi_builtins.ml", line 3347, characters 19-91
Called from Elpi__Runtime_trace_off.FFI.wrap_type_err in file "src/runtime_trace_off.ml", line 2071, characters 6-9
Called from Elpi__Runtime_trace_off.FFI.call.aux in file "src/runtime_trace_off.ml", line 2153, characters 32-92
Called from Elpi__Runtime_trace_off.FFI.call in file "src/runtime_trace_off.ml", line 2240, characters 21-70
Called from Elpi__Runtime_trace_off.Constraints.exect_builtin_predicate in file "src/runtime_trace_off.ml", line 3194, characters 20-77
Called from Elpi__Runtime_trace_off.Mainloop.make_runtime.run in file "src/runtime_trace_off.ml", line 3603, characters 19-84
Called from Elpi_util__Util.Fork.fork.ensure_runtime in file "src/utils/util.ml", line 466, characters 16-19
Re-raised at Elpi_util__Util.Fork.fork.ensure_runtime in file "src/utils/util.ml", line 475, characters 7-14
Called from Elpi__Runtime_trace_off.mk_outcome in file "src/runtime_trace_off.ml", line 3884, characters 14-23
Called from Elpi__Runtime_trace_off.execute_once in file "src/runtime_trace_off.ml", line 3901, characters 20-211
Re-raised at Elpi__Runtime_trace_off.execute_once in file "src/runtime_trace_off.ml", line 3906, characters 2-9
Called from Elpi__API.Execute.once in file "src/API.ml" (inlined), line 186, characters 4-55
Called from Coq_elpi_vernacular.run in file "src/coq_elpi_vernacular.ml", line 169, characters 11-53
Called from Coq_elpi_coercion_hook.elpi_coercion_hook in file "src/coq_elpi_coercion_hook.mlg", line 32, characters 8-53
Called from Coercion.inh_conv_coerce_to_gen in file "pretyping/coercion.ml", line 742, characters 33-126
Called from Coercion.inh_conv_coerce_to_gen in file "pretyping/coercion.ml", line 772, characters 6-106
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Pretyping.Default.pretype_var in file "pretyping/pretyping.ml", line 652, characters 21-78
Called from Pretyping.Default.pretype_app.pretype in file "pretyping/pretyping.ml" (inlined), line 792, characters 36-79
Called from Pretyping.Default.pretype_app.apply_rec in file "pretyping/pretyping.ml", line 881, characters 12-37
Called from Pretyping.Default.pretype_app in file "pretyping/pretyping.ml", line 903, characters 6-58
Called from Pretyping.Default.pretype_type in file "pretyping/pretyping.ml", line 1280, characters 21-70
Called from Pretyping.eval_type_pretyper in file "pretyping/pretyping.ml" (inlined), line 580, characters 2-49
Called from Pretyping.Default.pretype_prod.pretype_type in file "pretyping/pretyping.ml" (inlined), line 994, characters 41-89
Called from Pretyping.Default.pretype_prod in file "pretyping/pretyping.ml", line 1006, characters 26-65
Called from Pretyping.Default.pretype_type in file "pretyping/pretyping.ml", line 1280, characters 21-70
Called from Pretyping.eval_type_pretyper in file "pretyping/pretyping.ml" (inlined), line 580, characters 2-49
Called from Pretyping.Default.pretype_prod.pretype_type in file "pretyping/pretyping.ml" (inlined), line 994, characters 41-89
Called from Pretyping.Default.pretype_prod in file "pretyping/pretyping.ml", line 1006, characters 26-65
Called from Pretyping.Default.pretype_type in file "pretyping/pretyping.ml", line 1280, characters 21-70
Called from Pretyping.eval_type_pretyper in file "pretyping/pretyping.ml" (inlined), line 580, characters 2-49
Called from Pretyping.Default.pretype_prod.pretype_type in file "pretyping/pretyping.ml" (inlined), line 994, characters 41-89
Called from Pretyping.Default.pretype_prod in file "pretyping/pretyping.ml", line 1006, characters 26-65
Called from Pretyping.Default.pretype_type in file "pretyping/pretyping.ml", line 1280, characters 21-70
Called from Pretyping.eval_type_pretyper in file "pretyping/pretyping.ml" (inlined), line 580, characters 2-49
Called from Pretyping.Default.pretype_prod.pretype_type in file "pretyping/pretyping.ml" (inlined), line 994, characters 41-89
Called from Pretyping.Default.pretype_prod in file "pretyping/pretyping.ml", line 1006, characters 26-65
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1378, characters 2-57
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1397, characters 21-73
Called from Pretyping.understand_tcc in file "pretyping/pretyping.ml", line 1447, characters 20-71
Called from Vernacentries.check_may_eval in file "vernac/vernacentries.ml", line 1860, characters 17-54
Called from Vernacentries.translate_pure_vernac.(fun) in file "vernac/vernacentries.ml", line 2467, 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 21, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 160, characters 24-126
Called from Vernacinterp.with_fail in file "vernac/vernacinterp.ml", line 48, characters 12-16
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.with_fail in file "vernac/vernacinterp.ml", line 55, characters 57-75
Called from Vernacinterp.with_fail in file "vernac/vernacinterp.ml", line 64, characters 12-23
Called from Vernacinterp.interp_control_entry in file "vernac/vernacinterp.ml", line 89, characters 4-82
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 in file "vernac/vernacinterp.ml", line 204, characters 16-41
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml", line 218, characters 15-72
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2185, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 965, 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 2327, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2424, 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 79, characters 29-50
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 Util.try_finally in file "lib/util.ml", line 131, characters 16-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 135, characters 6-32
Called from Vernac.load_vernac_core.loop in file "toplevel/vernac.ml", line 121, characters 8-352
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 134, 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 210, characters 30-83
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 70, characters 18-78
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 126, characters 2-59
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

[gares]

Looks like a regression on the coq side, the catching anomaly thing in e 8.18.1 milestone. Could you do a cherry pick and test it.

[Tragicus]

It did not change anything.