Interpreting a casted term in the scope bound to its type if any

[herbelin]

This is a proposal in relation to the discussion at #6078.

It proceeds in several steps depending on taste:

• setting type_scope when casted by a sort
• removal of the then-redundant vernac-level notation casts in ssreflect.v
• interpreting any term casted with a type bound to a scope in this scope
• a start at interpreting any pattern casted with a type bound to a scope in this scope, as also discussed at ssreflect pollutes notation precedence space for colon #6078.

There are more to do about the last step but that will become easier in the context of the more regular parsing of patterns in #982.

Note 1: I have a terminology question: how to call the bind in Option? In which order should be its arguments? (I tentatively called it compose.)
Note 2 : This PR depends on #6133 (replaced by #18031) and #982 (merged) shall depend on it for interpreting casts in
patterns.

Fixes: #14959

Overlays (to be merged before the current PR)

• Adapting to interpretation of (x:T) now activating scope for T if any. rocq-community/corn#199
• Adapt to https://github.com/coq/coq/pull/6134 rocq-community/math-classes#118

[Zimmi48]

I have a terminology question: how to call the bind in Option? In which order should be its arguments? (I tentatively called it compose.)

I haven't checked how the other binds are called in the code base currently but I would be in favor of uniformity of naming. For instance, in Elm all the binds are called andThen: this particular one is Maybe.andThen (Maybe being the terminology inherited from Haskell to designate Option), and there is also Result.andThen, Task.andThen, etc.
So if the name bind is already used, then it could be used here as well.

As for the order of the arguments, the “standard” order coming from Haskell is to put the argument encapsulated in a monad first, and the function then, but Elm has recently decided to change this order for a very good reason: compatibility with the |> (pipe operator). This gives:

Just 1
|> Maybe.andThen (\x -> if x = 0 then Nothing else x + x) 
|> Maybe.map (\x -> x - 1)

But while I like this order of argument better, I think the most important thing is consistency. So if Coq has already got binds with the other order, keep the other order for this new bind as well (unless we change the order for all the binds at once).

[herbelin]

I have a terminology question: how to call the bind in Option? In which order should be its arguments? (I tentatively called it compose.)

I haven't checked how the other binds are called in the code base currently but I would be in favor of uniformity of naming.

There is already not a lot of uniformity. For instance the return in Option is make.

Anyway, there are many ways to look at an object. Shall we favor a name which reflect some intuition of the object, or another intuition? Shall we reflect algebraic properties of an object, but why such property and not another one.

But I think it is also important to share a common language, and that's why I preventively raised the question.

[maximedenes]

A rebase seems needed.

[herbelin]

This PR introduces incompatibilities in HoTT and math-classes:

• HoTT: a scope implicitly propagated to the body of a cast is not propagated any more. I guess @JasonGross, who asked for the current PR, is ok for a fix. However, it is unclear what to do. We had Notation "S / T" := (comma_category (S : CC_Functor' _ _) (T : CC_Functor' _ _)) and thus S and T in scope %functor inherited from comma_category. If I add a %functor around S and T, it is too strong as it recursively changes the scope towards the structure of S and T. One would need a way to say temporarily set %functor and there is no syntax for that. Maybe should we provide one?
• math-classes (diff): several instances did not need a cast, so I removed the cast. Other instances were expecting a cast to help type class inferences. I added an explicit %mc to enforce the scope as it was formerly. Don't know if it is ok for @spitters.

[spitters]

It's a small change. I can live with that for math-classes.
Could you send a PR when this gets merged?

[Zimmi48]

Just making sure: is this fix backward compatible?

[JasonGross]

What breaks if %functor is added in HoTT?

[JasonGross]

Looking at the commits to HoTT: oh this is interesting. I think the thing I actually want here is to be able to bind category_scope to object Cat (while leaving object_scope bound to object _), and have bound scopes added to the scope stack rather than having a separate local scope.

I'm also curious about the alternative of not removing the current local scope if no scope is bound to the type. What breaks if we do this instead?

[herbelin]

Looking at the commits to HoTT: oh this is interesting. I think the thing I actually want here is to be able to bind category_scope to object Cat (while leaving object_scope bound to object _), and have bound scopes added to the scope stack rather than having a separate local scope.

I'm sorry @JasonGross, but I don't know how to help here. I don't know HoTT well enough to understand the ins and outs of a choice or another. Maybe could you just tell me if you're ok with the patch or if you'd prefer another one.

I'm also curious about the alternative of not removing the current local scope if no scope is bound to the type. What breaks if we do this instead?

You mean as a general rule (rather than for the particular case of HoTT)?

Probably nothing would break further since this is the strategy applied up to now. I don't have a strong opinion. It looks a bit ad hoc to me but maybe it would be convenient in practice. I don't know if e.g. @ggonthier, who proposed the change, has an experience to share

[JasonGross]

@herbelin I'm willing to accept the patch. I'd still be interested in the feature I mentioned; shall I open a new issue to request the ability to do things like Bind Scope type_scope with (id Type).?

[herbelin]

I'd still be interested in the feature I mentioned; shall I open a new issue to request the ability to do things like Bind Scope type_scope with (id Type).?

Well, yes. (And this reminds me of similar requests for coercions.)

And, on my side, I wonder whether there would be some need or support for an explicit syntax for temporary scope or to-stack scope in situations where the other semantics is taken. The current syntax either adds the scope to the stack (term%scope in an expression), or makes it a temporary scope (as in Arguments foo x%scope.). Would it be useful to provide say term%%scope to tell temporary in expressions and Arguments foo x%!scope to tell to stack?

In particular, this is obviously related to #3990, though I feel that the examples in #3990 are asking for more typing invariant being propagated, something that can be achieved more easily with typeclass-based notations. Being short in available time, I'm stopping there. BTW, it would be useful to have a comparison of the advantages and drawbacks of scope-based vs typeclass-based notations (or maybe such comparison already exists?).

[maximedenes]

Note 2 : This PR depends on #6133 and #982 shall depend on it for interpreting casts in patterns.

Is it still the case? What is the current status of this PR?

[herbelin]

Is it still the case?

#6133 is closed and now part of this PR. For #982, I'll have to check but I suspect that it should be autonomous.

What is the current status of this PR?

There are still a few incompatibilities (in HoTT and formal-topology), so I wonder whether @JasonGross' proposition of a mixed strategy (i.e. propagating the surrounding temporary scope if the type is not bound to a scope) could be a good compromise. Somehow, more user feedback would be useful. Maybe should we explicitly notify some people, e.g. those who participated to #3990, to take part to the discussion (and at the same time I know that everyone is very busy...).

In any case, my current view is to take a couple of days for letting mature what could be the optimal policy.

[SkySkimmer]

In any case, my current view is to take a couple of days for letting mature what could be the optimal policy.

It has been a bit more than a couple days, any conclusions?

[herbelin]

@herbelin CI green here, I'd like to complete the doc, add a changelog entry and merge if you agree?

OK on my side.

[proux01]

I'll merge by the end of next week if there are no more comments.

[jfehrle]

Wording suggestions

[proux01]

Let's finally merge this almost six years old PR.

@coqbot merge now