coq.typecheck-indt-decl failing where it succeeds in plain Coq

[proux01]

I stumbled onto the following while attempting to port CoqEAL to param2:

From elpi Require Import elpi.

Definition myType := Type.
Variant indd : myType := Indd : indd.

Definition myType_R u v := u -> v -> Type.

(* the following works *)
(* Inductive indd_R : myType_R indd indd := *)
(*   Indd_R : indd_R Indd Indd. *)

Elpi Command foo.
Elpi Accumulate "
main _ :-
  std.assert-ok! (coq.typecheck-indt-decl (inductive ""indt_R"" tt
    (arity {{ myType_R indd indd }})
    c1 \
      [ constructor ""Indd_R"" (arity {{ lp:c1 Indd Indd }}) ])) ""error"".
".
(* this fails *)
Fail Elpi foo.

(* but the following works *)
Elpi Command bar.
Elpi Accumulate "
main _ :-
  std.assert-ok! (coq.typecheck-indt-decl (inductive ""indt_R"" tt
    (arity {{ indd -> indd -> Type }})  % same with this beta-reduced
    c1 \
      [ constructor ""Indd_R"" (arity {{ lp:c1 Indd Indd }}) ])) ""error"".
".
Elpi bar.

[gares]

The problem seems to be here:

coq-elpi/elpi/coq-lib.elpi

Lines 356 to 360 in c40e913

	coq.typecheck-indt-decl-c.unify-arrow-tgt I P A Concl D :-
	coq.count-prods A N,
	coq.mk-n-holes {calc (N + P)} Args,
	coq.mk-app I Args IArgs,
	coq.unify-eq Concl IArgs D.

I guess adding an extra rule calling whd1 to reduce the inductive arity to a spine or prod may suffice.

[gares]

I mean, it is probably count-prods that should reduce.