Inherit implicit arguments in coercions to Funclass (fixes/grants #5527) by herbelin · Pull Request #11327 · rocq-prover/rocq

herbelin · 2019-12-22T15:42:28Z

Kind: Enhancement

Fixes / closes #5527

The PR includes some commits from #11326 (merged).

This is a proposal so as to inherit implicit arguments in the presence of coercions to Funclass.

For elaboration, we work at the level of pretyping.ml to insert implicit arguments whenever a coercion to Funclass is used. In particular, we need to move impargs.ml in pretyping so that it can be called from coercion.ml. @ejgallego: are you ok? (Note that it would be natural to merge impargs.ml and arguments_renaming.ml. The latter is in pretyping so that it can be called in typing.ml. This is a second reason to move impargs.ml into pretyping, even if it is bit disappointing to see that implicit arguments impact typing.)

TODO: understand better inheritance of interpretation scopes. With this PR, interpretation scopes are inherited (for printing) from the coercion scopes. Before, the "extra scopes" of the main argument of the coercion were used instead (for printing). As far as I understand, the point of "extra scopes" is to reflect the scopes of the coercions to Funclass, but that would need to be checked. (Eventually, the "extra scopes" hack could also be removed.) Extra scopes at interning are unchanged.

Added / updated test-suite
Entry added in the changelog

Added: To improve compatibilities, a temporary fallback on discarding implicit arguments has been implemented, together with a warning. It fails to detect cases where a second coercion to Funclass can (unexpectedly) be applied in a row.

herbelin · 2020-02-18T14:35:14Z

Report on the failures: the compatibility test works pretty well. Only the case where a second coercion to Funclass is applicable fails to be detected. This happens in two cases:

Iris: the fix is to replace some F into F which is expected
Unimath: the fix is more complicated. Due to the implicit arguments, the coercion is not correctly applied by exact and I replaced some pr1 a c (the c is extra) with disp_functor_on_objects (pr1 a).

Here is for the record a simplified example of what exact should be able to do in this PR, in the presence of implicit arguments:

Axiom f : nat -> forall {B}, list B -> nat.
Coercion f : nat >-> Funclass.
Goal list bool -> nat.
Fail exact 0. (* coercion not inserted because its implicit argument is missing for typing *)
exact (f 0).

herbelin · 2020-02-18T14:43:19Z

Yet another question. If I have:

Axiom f : nat -> forall {n:nat}, n=n.

should I accept f to be a coercion to Funclass or do I expect for it to be to Funclass that at least one argument is non-implicit? I don't see examples where I might want a coercion to Funclass and not expecting an explicit argument. So, this seems reasonable to me that coercions skip the implicit arguments and that the following instead work: (?)

Axiom f : nat -> forall {n:nat}, n=n.
Coercion f : nat >-> eq.

Maybe, @pi8027, did you already encounter such issues?

gares · 2020-02-18T15:02:35Z

I've mixed feelings about this feature, especially in his cost/benefit.
The cost is a more tight coupling between two components, I could live with that.

The benefits are totally unclear to me. In particular quantifying in the middle of a spine of arrows is weird, it seems more natural to put the type of the term acting as a coercion in a prenex form, i.e. put the implicit argument before the term being casted. To me the coercion is a "technical term" (that the user is not even supposed to see) so requiring it to have a specific shape does not seem an hard requirement (we already require it to have some other properties for example).

herbelin · 2020-02-18T16:01:15Z

@gares: @tchajed gave an example at #5527 and there are examples in Iris, UniMath, suspectingly in mathcomp too. You are basically liable to have implicit arguments in a coercion to Funclass anytime you want a coercion to a field which has dependent arguments.

See for instance a comment mentioning this issue in Iris' file ofe.v:

(** Note that the implicit argument [Cofe A] is not taken into account when
[oFunctor_diag] is used as a coercion. So, given [F : oFunctor] and [A : ofeT]
one has to write [F A _]. *)

tchajed · 2020-02-18T16:06:50Z

Yes, @gares, from a benefits perspective this feature would be awesome, though I can't comment on how much complexity it adds.

The issue is basically that you effectively can't have Funclass coercions to polymorphic functions; it actually exposes that you're using a coercion because you need these _ arguments. My example in #5527 is a reduced artificial example (and this is long enough ago that I've forgotten what my real use case was at the time), but the Iris example is a good realistic one.

herbelin · 2020-02-18T17:57:59Z

@gares: if you want examples in MathComp, look for the warning funclass-coercion-implicit-arguments-skipping-deprecated in the CI for mathcomp (there are about 40 of them). The first example is the coercion apply in gfunctor.v, whose first argument is implicit. As a consequence, F gT G could be simplified into F G in line 251 of gfunctor.v.

ppedrot · 2020-02-19T10:01:35Z

pretyping/pretyping.ml

+              warn_tolerance_no_coercion_implicit_argument ?loc (!!env,sigma,coe);
+              x
+            with e when CErrors.noncritical e ->
+              raise e'


Instead of doing this try-with dance, you should return an algebraic type in f, catching the exception there. Using exceptions for control flow is a recipe for a disaster.

Is the risk that warn itself raises an error?

I can certainly use a sum type instead, but this is anyway supposed to be temporary and I fail to see how much it really matters here, even though I'm ready to follow recommended common practices which improve our synergy.

@ppedrot: I experimented using a sum type. It is actually nicer than what I had thought!

amahboubi · 2020-02-19T13:34:26Z

@gares, your suggestion to put the quantification in prenex position works, but does not survive composition.
So it seems to me that it is a clear improvement. However, the gfunctor file is an infrastructure library and probably not one as curated as other files in mathcomp. As far as I can tell (but I did not inspect the warnings), this does not impact "client code" of this infrastructure. So I am not sure that this would bring us a significant gain.

pi8027 · 2020-02-19T13:58:10Z

Yet another question. If I have:
Axiom f : nat -> forall {n:nat}, n=n.
should I accept f to be a coercion to Funclass or do I expect for it to be to Funclass that at least one argument is non-implicit? I don't see examples where I might want a coercion to Funclass and not expecting an explicit argument. So, this seems reasonable to me that coercions skip the implicit arguments and that the following instead work: (?)
Axiom f : nat -> forall {n:nat}, n=n.
Coercion f : nat >-> eq.

IMO, declarations of implicit coercions should be independent of Arguments declarations. One may change that implicit argument n to an explicit argument after the above coercion declaration of f, and then that coercion does not make much sense anymore.

herbelin · 2020-02-19T19:25:06Z

@amahboubi

As far as I can tell (but I did not inspect the warnings), this does not impact "client code" of this infrastructure.

Would it be ok that the warning is temporary and that taking implicit arguments of coercions to Funclass into account eventually becomes the default rule?

@pi8027

IMO, declarations of implicit coercions should be independent of Arguments declarations. One may change that implicit argument n to an explicit argument after the above coercion declaration of f, and then that coercion does not make much sense anymore.

That's right.

One could otherwise give to:

Axiom f : nat -> forall (n:nat), n=n.
> Coercion f : nat >-> eq.

the meaning of declaring fun x => f x _ as being the coercion, granting the wish to see it as coercion to eq. But anyway, this is probably minor.

ejgallego · 2020-02-20T19:18:08Z

pretyping/pretyping.ml

+        | Some (coe,_) ->
+          let c',rest',some_change = insert_impargs ?loc impls c rest in
+          if not some_change then f c rest else
+          let g c rest = try Inl (f c rest) with e when CErrors.noncritical e -> Inr e in


Please avoid generic catch-all of exceptions.

Sorry, I did not get it. What is your suggestion?

As @ppedrot suggested before f should not raise and instead return an algebraic type; the code indeed looks pretty hard to reason as calls to user_err are later absorbed.

Moreover the reraise is likely incorrect below, as in it loses information. That should not matter for Coq, but unfortunately that may not be the case.

As @ppedrot suggested before f should not raise and instead return an algebraic type

I don't see how I can avoid f to raise an exception. f is calling unify, pretype, all kinds of function which possibly raise an exception w/o having control on where it is raised.

as in it loses information

You mean information of the trace?

By the way, I meant reraising e' not e. Changing.

I don't see how I can avoid f to raise an exception. f is calling unify, pretype, all kinds of function which possibly raise an exception w/o having control on where it is raised.

Do we have an specification of what these functions can raise? Indeed they should not raise except on error, and if there is an error there why we absorb it? IMHO we really have a mess in the codebase. I cannot understand for example why here all errors are actually absorbed, that seems wrong in a few cases, like for example a missing lib by Coqlib etc... Yeah our notion of "recoverable error" is pretty ill-defined.

I know that is it not easy to fix this, but at least IMO in new code the try ... with ... block should be pushed to the inner boundaries so they act as wrappers of the raising functions and turn the caught exception into something sensible.

You mean information of the trace?

Of the trace and anything else users attached to it using our dangerous Exnifo API.

Do we have an specification of what these functions can raise?

You know how helpful is OCaml to inform about side effects!

In any case, this could be a catch of precatchable_exception instead of noncritical but I'd bet that this would not make a difference.

Are you suggesting that we should pass not only states but exceptions in purely functional style?

if there is an error there why we absorb it

It's done that way to implement the compatibility mode.
IMO this is the wrong way to work, if we want the PR's feature we should put an option to disable it and deprecate the option. Then we don't need to catch exceptions here.

Having a warning with a location is useful to upgrade. Then, we could do an automatic translation, the same way the python script replaced automatically references to deprecated aliases in 8.9. An option is possible in parallel.

@ejgallego: I added an Exninfo.capture to not "lose information". Otherwise, I don't know how I can reasonably avoid catching all non-critical exceptions. As the code is written and as OCaml is designed, I have no precise idea of what exceptions typing functions exactly raise. How to control this would go well beyond the scope of the PR (starting with a careful documentation of these functions, eventually ensuring, e.g., that a typing function raises only PretypeError!?).

In any case, in a context of extensibility of exceptions, we will certainly have at some point to clarify whether we characterize exceptions positively (i.e. knowing the list of exceptions a function can raise) or negatively (i.e. knowing the list of exceptions a function should not raise).

coqbot-app · 2021-12-13T02:15:54Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

coqbot-app · 2022-01-12T02:18:51Z

This PR was not rebased after 30 days despite the warning, it is now closed.

…account.

… to Funclass. Inherit also interpretation scopes of the coercion.

…funclass coercions.

JasonGross · 2022-01-26T14:34:19Z

TODO: understand better inheritance of interpretation scopes. With this PR, interpretation scopes are inherited (for printing) from the coercion scopes. Before, the "extra scopes" of the main argument of the coercion were used instead (for printing). As far as I understand, the point of "extra scopes" is to reflect the scopes of the coercions to Funclass, but that would need to be checked.

I thought extra scopes were also used in the case of polymorphic functions which might be instantiated with arrow types.
My inclination here is to keep the old behavior; as I understand it, the old behavior has the same scopes used for printing and parsing, while the new behavior makes them diverge; is that correct?

JasonGross · 2022-01-26T15:39:15Z

Summary of my position after the Coq call:
I like this feature, I think it should ideally be done in a way that doesn't entangle globalization with typing more.
Hence the scopes should not come from the coercion (neither in parsing nor printing, unless coercions are printed).

I suggested the possibilities of:

when you define either a coercion to funclass or a constant, or change the scopes on either one, check if the scopes align, and emit a warning if they don't
instead of (or in addition to) emitting a warning, extras scopes to constants could be assigned automatically based on the coercion (this could even be done sort-of-dynamically like scopes bound to types; in fact, I think the same mechanism can be reused, where automatic scopes are looked up based on scopes bound to types and extra scopes are looked up automatically based on the coercion graph; as I write this out, I'm coming to like this idea more and more)

coqbot-app · 2022-03-16T02:27:33Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

coqbot-app · 2022-04-15T02:41:36Z

This PR was not rebased after 30 days despite the warning, it is now closed.

herbelin added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: elaboration The elaboration engine, also known as the pretyper. part: printer The printing mechanism of Coq. labels Dec 22, 2019

herbelin added this to the 8.12+beta1 milestone Dec 22, 2019

herbelin requested a review from mattam82 as a code owner December 22, 2019 15:42

herbelin force-pushed the master+coercions-inherit-implicits branch 2 times, most recently from 99cbb4a to a3784e3 Compare December 22, 2019 18:35

herbelin requested review from a team and ppedrot as code owners December 22, 2019 18:35

SkySkimmer added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Feb 10, 2020

herbelin force-pushed the master+coercions-inherit-implicits branch from a3784e3 to d45f702 Compare February 18, 2020 06:10

herbelin requested review from a team as code owners February 18, 2020 06:10

coqbot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Feb 18, 2020

herbelin mentioned this pull request Feb 18, 2020

Add support for instantiating non dependent implicit arguments by position #11099

Merged

3 tasks

ppedrot reviewed Feb 19, 2020

View reviewed changes

SkySkimmer added the needs: benchmarking Performance testing is required. label Feb 19, 2020

herbelin force-pushed the master+coercions-inherit-implicits branch from d45f702 to d1be1a4 Compare February 20, 2020 18:21

ejgallego suggested changes Feb 20, 2020

View reviewed changes

herbelin reopened this Oct 29, 2021

herbelin force-pushed the master+coercions-inherit-implicits branch from 4adb443 to c59b72d Compare October 29, 2021 08:15

herbelin requested a review from a team as a code owner October 29, 2021 08:15

coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Oct 29, 2021

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 11, 2021

coqbot-app bot added the stale This PR will be closed unless it is rebased. label Dec 13, 2021

coqbot-app bot closed this Jan 12, 2022

herbelin reopened this Jan 12, 2022

herbelin added 8 commits January 12, 2022 10:49

Moving impargs.ml in pretyping for use in coercion.ml.

3058d55

Elaboration: Taking implicit arguments of coercions to Funclass into …

bb8dfa9

…account.

Inherit implicit arguments when printing terms with omitted coercions…

6747512

… to Funclass. Inherit also interpretation scopes of the coercion.

Compatibility: temporary warning when skipping implicit arguments of …

faf06c4

…funclass coercions.

Adding an option Implicit Arguments Coercion Inheritance

e0abff1

Overlay for UniMath

e223521

Adding List.sep_first.

cb0269b

Reasoning abstractly over whether a coercion is a prim proj or not.

6e2aecb

herbelin force-pushed the master+coercions-inherit-implicits branch from c59b72d to 6e2aecb Compare January 12, 2022 10:45

coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Jan 12, 2022

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Feb 14, 2022

Alizter mentioned this pull request Mar 12, 2022

[coercions] Remove uniform inheritance condition #15789

Merged

3 tasks

coqbot-app bot added the stale This PR will be closed unless it is rebased. label Mar 16, 2022

coqbot-app bot closed this Apr 15, 2022

Conversation

herbelin commented Dec 22, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

herbelin commented Feb 18, 2020

Uh oh!

herbelin commented Feb 18, 2020

Uh oh!

gares commented Feb 18, 2020

Uh oh!

herbelin commented Feb 18, 2020

Uh oh!

tchajed commented Feb 18, 2020

Uh oh!

herbelin commented Feb 18, 2020

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

amahboubi commented Feb 19, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Feb 19, 2020

Uh oh!

herbelin commented Feb 19, 2020

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

herbelin Aug 26, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

coqbot-app bot commented Dec 13, 2021

Uh oh!

coqbot-app bot commented Jan 12, 2022

Uh oh!

JasonGross commented Jan 26, 2022

Uh oh!

JasonGross commented Jan 26, 2022

Uh oh!

coqbot-app bot commented Mar 16, 2022

Uh oh!

coqbot-app bot commented Apr 15, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

11 participants

herbelin commented Dec 22, 2019 •

edited

Loading

amahboubi commented Feb 19, 2020 •

edited

Loading

herbelin Aug 26, 2021 •

edited

Loading