[subsumed] Ssreflect.v: drop a cast notation useless since 8.5

[herbelin]

This is a concrete proposal to fix issue #6078 (see discussion there).

[maximedenes]

I have to catch up with the discussion, so I'm not sure if this is expected to break mathcomp, but it seems it is the case.

[gares]

The incriminating line is:
https://github.com/math-comp/math-comp/blob/master/mathcomp/fingroup/presentation.v#L162
Hum, I guess the notation in ssreflect.v sets a level, hence this other notation goes trough.
I've no clue if setting a notation level in presentation.v can fix the issue...

[herbelin]

Indeed, I suspect that changing it to

Notation "x : p" := (Generator (x : p))
  (at level 100, right associativity,
   format "'[hv' x '/ '  :  p ']'") : group_presentation.

would make it work. What do you think?

(edited for typo)

[gares]

I've no clue, I think you should try with an overlay

[herbelin]

Hi, modifying presentation.v is actually not enough. There is another incompatibility at the end of BGappendixC.v (a done is failing).

The reason is that there is still a difference between the native parsing rule and the user-level defined one in ssreflect.v. The body of the native cast is interpreted in the same local scope as the cast itself while the redefined one interprets the body in the empty local scope, with a difference in a situation like:

Notation "#" := true.
Notation "#" := false : bool_scope.
Check eq_true (#:bool). (* false *)
Notation "x : T" := (x : T) (at level 100, right associativity) : core_scope.
Check eq_true (#:bool). (* true *)

#6134 is precisely changing this, using the cast to set the local scope and unsetting the local scope if the type is not associated to a scope. However, this is a change of semantics. So, what to do? Maybe the simplest would be for 8.7.1 and #6078 to move the ssreflect cast notations in the copy of ssreflect.v which is in math-comp (if ever it is loaded)? Any opinion?

Added: In the precise case under consideration in BGappendixC.v (subterm <[1:F]> in the definition of finFieldImage, where 1 has different interpretations depending on scope), I see no evidence that one scope semantics is better than the other. I'm just reporting the existence of an incompatibility.

[Zimmi48]

In my opinion, this "bug" could be viewed as an enhancement request and is not essential to have in 8.7.1.
It is not essential to VST developers and is not new in 8.7 (AFAIK and contrary to what was initially reported).
Consequently, I would say that it is not a big deal to have a change of semantics, but this PR should target 8.8.

[herbelin]

@Zimmi48: you're right. So, maybe can I merge this with #6134, if no objections.

Then, math-comp can decide whether an overlay in presentation.v is enough or if a different approach is better.

[gares]

#6134 is precisely changing this

Does this mean that with #6134 there is no need for an overlay? I.e. that removing the notation from ssreflect.v generates no failure?

[herbelin]

Cross posting: With #6134, the overlay would still be needed in presentation.v (because it declares a notation assuming that a parsing rule has already been given which would not be the case anymore), but the other failure in BGappendixC.v (difference in interpretation scopes) should not happen anymore.

[JasonGross]

Is "local scope" the innermost bound scope, separate from the scope stack that is modified by Open Scope and %? (And why are these separate things? And is the fact that they are separate things mentioned anywhere in the manual?)

[herbelin]

The reference manual says: "When interpreting a term, if some of the arguments of qualid are built from a notation, then this notation is interpreted in the scope stack extended by the scope bound (if any) to this argument. The effect of the scope is limited to the argument itself. It does not propagate to subterms but the subterms that, after interpretation of the notation, turn to be themselves arguments of a reference are interpreted accordingly to the arguments scopes bound to this reference.". Maybe would you like that it is more strongly said as different?

This temporary scope is not formally called "local". In the implementation, it is called the temporary scope.

Why are there different? Both are useful I think. There was an issue which I don't find again about making temporary scopes extend to the whole subterm. I made the experience once but it is highly incompatible.

[herbelin]

So, maybe can I merge this with #6134, if no objections.

I'm assuming no objections and closing.