Fix occurrence checker not checking evar insts

[Tragicus]

Reopening of #18966.

Fixes / closes #18965

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[ppedrot]

@coqbot run full ci

[Tragicus]

I am not sure I understand the third test in ValidateProof.v, the proof contains no match on f and is typeable of the correct type. Nevertheless, for compatibility I restored the missing check.

[ppedrot]

@coqbot run full ci

[ppedrot]

This is wrong, retyping assume the argument to be well-typed but here we precisely don't know about ty yet.

[SkySkimmer]

also maybe we should be checking the evar arguments instead of the substituted type? ie if we have an evar ?e : nat with context x : nat, S ?e@{x := true} would be accepted by typing.ml in master but the (valid) instantiation ?e := x would then turn it into an invalid term S true.

[Tragicus]

[at]SkySkimmer Is this (1d73de2) what you mean?

[ppedrot]

This is closer but still not enough. You need to check that the telescope type associated to the evar is compatible with the argument types, i.e. basically the same as the application rule.

[Tragicus]

Ah, yes, thank you. I know about existential_type which if I understand correctly is the substituted type and evar_concl which according to the code of existential_type looks like it is the non-substituted type but without the telescope. Can I find the telescope somewhere? No, wait, nevermind, I did not look hard enough at evar_info, let me try again.

[Tragicus]

No sorry, I am lost. I thought Evd.evar_context might be it, but it does not have the correct length, I find more items in evar_context than in the arguments list. May I ask for a hint?

[SkySkimmer]

Evd.evar_filtered_context I believe

[Tragicus]

Yes, that is it, thank you. I assume the LocalDef declarations are supposed to match the Default from the arguments list? Nevermind, I tested and they are not aligned. Are they not supposed to be?

[Tragicus]

The issue in Case13.v looks a lot like a bug in the compilation of matches. In prepare_predicate_from_arsign_tycon, the let p = predicate 0 c in line changes the argument of the evar c by something else, but this argument can appear in the type of other arguments which are not changed, so p is ill-typed.
More precisely,
env = [] [(z : ?X60) (Q : ?X61@{__:=z}) (y : K CSTR.bool._0._1 z) (f : forall z : bool, Q z)]
c = ?X64@{{__:=#4; __:=#3; __:=#2; __:=#1}
env' = [] [(z : ?X60) (Q : ?X61@{__:=z}) (y : K CSTR.bool._0._1 z) (f : forall z : bool, Q z) (_ _ : bool) (y : K #2 #1)]
p = ?X64@{__:=#2; __:=#6; __:=#5; __:=#4}