Infer the relevance of inductive parameters by retyping

Changelog.md

@@ -6,6 +6,9 @@
   parameter, in both directions (reading a declaration back was raising
   `Invalid_argument("index out of bounds")` from the kernel, printing one
   was producing an ill-typed declaration)
+- Fix the relevance mark of `parameter` binders in inductive declarations: it
+  is now inferred by retyping instead of being left to the (relevant) mark
+  carried by the name, which the kernel rejects for a parameter in `SProp`
 
 ### API:
 - New `coq.string->name-irrelevant`, the counterpart of

src/rocq_elpi_HOAS.ml

@@ -3336,6 +3336,9 @@ let readback_arity ~depth coq_ctx constraints state t =
         let state, name, gl0 = in_coq_annot ~depth state name in
         let state, imp = in_coq_imp ~depth state imp in
         let state, ty, gls = lp2constr coq_ctx ~depth state ty in
+        (* The kernel checks a parameter's mark against the sort of its type, so
+           the unset mark a name carries will not do. *)
+        let name = relevance_of_binder coq_ctx.env (get_sigma state) name ty in
         let e = Context.Rel.Declaration.LocalAssum(name,ty) in
         aux_lam e coq_ctx ~depth (e :: params) (manual_implicit_of_binding_kind (Context.binder_name name) imp :: impls) state (gl0 :: gls :: extra) decl
     | E.App(c,ty,[]) when c == arityc ->
@@ -3739,6 +3742,9 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         let state, name, gl0 = in_coq_annot ~depth state name in
         let state, imp = in_coq_imp ~depth state imp in
         let state, ty, gls = lp2constr coq_ctx ~depth state ty in
+        (* The kernel checks a parameter's mark against the sort of its type, so
+           the unset mark a name carries will not do. *)
+        let name = relevance_of_binder coq_ctx.env (get_sigma state) name ty in
         let e = Context.Rel.Declaration.LocalAssum(name,ty) in
         aux_lam e coq_ctx ~depth (e :: params) (manual_implicit_of_binding_kind (Context.binder_name name) imp :: impls) state (gls :: extra) decl
     | E.App(c,id,[fin;arity;rest])

tests/test_HOAS.v

@@ -1021,3 +1021,32 @@ Elpi Query lp:{{
   coq.env.add-const "sprop_after_fix" Body1 _ @transparent! _.
 }}.
 
+(* -------- Relevance of inductive parameters -------- *)
+
+(* coq.env.add-indt: infer a parameter's relevance from its type *)
+Elpi Query lp:{{
+  coq.locate "sTrue" (indt ST),
+  Decl =
+    (parameter "proof" explicit (global (indt ST)) proof\
+      inductive "sprop_parameter_inductive" tt (arity {{ Type }}) ind\
+        [constructor "sprop_parameter_constructor"
+           (arity ind)]),
+  std.assert-ok! (coq.elaborate-indt-decl-skeleton Decl Elaborated)
+    "failed to elaborate SProp-parameter inductive",
+  coq.env.add-indt Elaborated _.
+}}.
+
+(* coq.env.add-indt: same, for a parameter of an arity *)
+Elpi Query lp:{{
+  coq.locate "sTrue" (indt ST),
+  Decl =
+    (inductive "sprop_arity_parameter_inductive" tt
+      (parameter "proof" explicit (global (indt ST)) proof\
+        arity {{ Type }}) ind\
+        [constructor "sprop_arity_parameter_constructor"
+           (parameter "proof" explicit (global (indt ST)) proof\
+             arity (app [ind, proof]))]),
+  std.assert-ok! (coq.elaborate-indt-decl-skeleton Decl Elaborated)
+    "failed to elaborate SProp-arity-parameter inductive",
+  coq.env.add-indt Elaborated _.
+}}.