Infer the relevance of inductive parameters by retyping

[JasonGross]

parameter binders of an indt-decl built from Elpi receive a fresh, unconstrained relevance variable. The kernel rejects parameters whose type lives in SProp:

Inductive sTrue : SProp := sI.

Elpi Query lp:{{
  coq.locate "sTrue" (indt ST),
  Decl =
    (parameter "proof" explicit (global (indt ST)) proof\
      inductive "i" tt (arity {{ Type }}) ind\
        [constructor "k" (arity ind)]),
  std.assert-ok! (coq.elaborate-indt-decl-skeleton Decl E) "elaboration failed",
  coq.env.add-indt E _.
}}.

Error: Binder (proof : "sTrue") has relevance mark set to relevant but was
expected to be irrelevant (maybe a bugged tactic).

The same happens for parameter binders inside an arity. coq.elaborate-indt-decl-skeleton succeeds, but coq.env.add-indt fails, and Elpi surface syntax cannot specify parameter relevance.

Both readback sites—readback_arity and the inductive_parameterc case of lp2inductive_entry—now recompute the mark from the parameter type's sort with Retyping.get_sort_of, after reading back the type. If retyping raises, they retain the name's mark. This matches the kernel check; types in Type or Prop still yield Relevant.

tests/test_HOAS.v covers an SProp declaration parameter and an SProp arity parameter used by a constructor. Both fail on master with the error above and succeed with this change.

Wordsmithed by Codex.

[gares]

This approach is worrying, since retyping can be expensive.
I'd rather have the user elaborate a term and get the relevance fixed for him, rather than having it implicitly done at each API call that crosses the language boundary.

[JasonGross]

I've done some rebasing. Note that retyping is only for the parameters of inductives, so I don't think it can be that expensive. If you want the user to retype, I think we'd need to make parameters carry the relevance instead of just the name, but this seems kind-of awkward for the user. What do you think?

[gares]

right, I find that sticking the relevance in the names was a hack in the first place, both in rocq and elpi.
another option is to not-retype, but consider as irrelevant only stuff like (A : (T : SProp)) with an explicit cast to sprop.
we do the same for lambdas (if the type is cast to sprop then we override the relevance).
WDYT?