Stream: Coq users

Topic: A better type ascription syntax `foo : bar`

Paolo Giarrusso (Apr 09 2021 at 13:11):

As some might know, if inference fails on foo in a statement, writing foo : bar to help inference comes back to bite you. Could that be fixed?

Paolo Giarrusso (Apr 09 2021 at 13:17):

I've just explained the pitfall to a colleague. What I (or a typical user) wants is "produce foo but use bar to help inference", but the result they get still contains the ascription. Hence _some_ tactics (IME, rewrite) might fail to find occurrences of foo : bar in the goal (because there are none!)

Enrico Tassi (Apr 09 2021 at 13:19):

Does SSR's rewrite have this problem too?

Paolo Giarrusso (Apr 09 2021 at 13:20):

not sure but I expect yes

Paolo Giarrusso (Apr 09 2021 at 13:21):

and syntactic matching feels too common in Coq to live with casts

Michael Soegtrop (Apr 09 2021 at 13:22):

Not sure I understand you: are you saying that the type cast should be removed after successful inference or do you say that rewrite should be smarter? I guess you will need the cast during Qed time if you did need it during proof term construction.

Paolo Giarrusso (Apr 09 2021 at 13:22):

what stdpp and Iris do (I suspect for this reason, but haven't confirmed) is write implicit arguments by hand — they even have dedicated syntax for _all_ operators.

Paolo Giarrusso (Apr 09 2021 at 13:23):

it should be removed after inference

Michael Soegtrop (Apr 09 2021 at 13:24):

Won't you have issues during Qed then?

Paolo Giarrusso (Apr 09 2021 at 13:24):

and I must have been unclear, because it seems clear you don't need these casts it at qed time

Paolo Giarrusso (Apr 09 2021 at 13:24):

this is not in the proof but in statements

Michael Soegtrop (Apr 09 2021 at 13:24):

Ah ok, I see.

Paolo Giarrusso (Apr 09 2021 at 13:25):

I mean, you could do the same in proofs, since these casts are about inference, not those produced by simpl/compute/vm_compute/...

Paolo Giarrusso (Apr 09 2021 at 13:35):

an example of the disambiguation is https://gitlab.mpi-sws.org/iris/stdpp/-/blob/5843163bd51a5f1a7310ffb64bda3b4c6bb50c0c/theories/coGset.v#L192:

Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
  x ∈@{C} coGset_to_top_set X ↔ x ∈ X.

instead of

Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
  x ∈ (coGset_to_top_set X : C) ↔ x ∈ X.

where ∈@{C} is a variant of ∈ to specify C as an implicit argument

Paolo Giarrusso (Apr 09 2021 at 13:36):

(I'll admit that this isn't enough to show problems with rewrite or auto; this felt like a known problem which I knew about, but if it isn't I can investigate)

Michael Soegtrop (Apr 09 2021 at 13:44):

I am still struggling to understand the connection: the @ variant of the ∈ infix operators is required to avoid the : C type ascription because it would later make pattern matching for a rewrite more difficult?

Pierre-Marie Pédrot (Apr 09 2021 at 13:46):

@Paolo Giarrusso you can probably write a clever notation with tactic in terms to emulate a transparent cast.

Pierre-Marie Pédrot (Apr 09 2021 at 13:47):

We have already a bit of machinery to work around casts but it's fragile.

Pierre-Marie Pédrot (Apr 09 2021 at 13:47):

I believe that we should not try to hide this complexity from the user and clearly delineate "kind-of-proof-relevant" casts with mere type annotations.

Pierre-Marie Pédrot (Apr 09 2021 at 13:48):

(notwithstanding the fact casts are also heavily used in the legacy unification engine for horrible reasons)

Pierre-Marie Pédrot (Apr 09 2021 at 13:55):

If we want to introduce a language feature it might be yet another occasion to reuse the Program cast syntax

Meven Lennon-Bertrand (Apr 09 2021 at 14:19):

This might be naïve, but could it be possible to keep these kind of ascriptions around for typing purposes, but ignore them when comparing terms? I have used this trick on paper exactly to avoid the problem you describe of two terms not being considered equal/convertible because they have different casts in them.

Pierre-Marie Pédrot (Apr 09 2021 at 14:25):

define "comparing"

Pierre-Marie Pédrot (Apr 09 2021 at 14:25):

(ftr we already skip cast nodes in all equality functions I know of in the codebase)

Meven Lennon-Bertrand (Apr 09 2021 at 14:26):

Ah, that is what I meant

Meven Lennon-Bertrand (Apr 09 2021 at 14:28):

But then how come they can lead rewrite astray if they are ignored when comparing terms?

Pierre-Marie Pédrot (Apr 09 2021 at 14:28):

because term equality is far to be pattern recognition

Pierre-Marie Pédrot (Apr 09 2021 at 14:29):

term equality is a somewhat easy problem, although we already have way too many ways to define it.

Pierre-Marie Pédrot (Apr 09 2021 at 14:29):

easy when compared to pattern recognition which has a crazy number of moving parts

Meven Lennon-Bertrand (Apr 09 2021 at 14:29):

Everything is simple in the marvelous world of paper :upside_down:

Pierre-Marie Pédrot (Apr 09 2021 at 14:29):

(pattern recognition contains unification so this gives you a lower bound)

Pierre-Marie Pédrot (Apr 09 2021 at 14:31):

my personal take on that is that the problem is not so much rewrite being sensitive to casts than the vast discrepancy we can observe in the handling of cast nodes

Pierre-Marie Pédrot (Apr 09 2021 at 14:31):

(hint: this reminds me of the primitive projection mess)

gallais (Apr 09 2021 at 14:52):

Naïve question: what is wrong with defining the identity function as an annotation gadget & using unfold to magic it away when needed?

Definition Identity (A : Type) (a : A) : A := a.
Notation "A ∋ a" := (Identity A a) (at level 3).

Goal forall n, nat ∋ n = n + O.
intros. unfold Identity.

(disregard the random level, I couldn't be bothered to look up how to make it right associative)

Pierre-Marie Pédrot (Apr 09 2021 at 15:03):

It won't work for OP's use because he wants to pass such terms to tactics.

gallais (Apr 09 2021 at 15:26):

Right this seems to work

Definition Identity (A : Type) (a : A) : A := a.

Ltac Ann A a :=
  let annotated := let h := fresh "H" in pose (h := Identity A a); exact a in
  let val := eval cbn zeta in ltac:(annotated) in
  exact val.

Notation "A ∋ a" := ltac:(Ann A a) (at level 3).

Goal forall n, n = n + O.
intro n. rewrite plus_n_O with (n := nat ∋ n).

But then again my example is super naïve and Coq already knew that n was of type nat so I don't know whether it'd work in OP's case.

Pierre-Marie Pédrot (Apr 09 2021 at 16:55):

No, unfortunately IIUC ltac quotations force to evaluate the term first, so you lose the typing constraint. You might be able to do that in Ltac2 because you have access to the untyped term in the quotation there.

Paolo Giarrusso (Apr 09 2021 at 16:57):

I agree that the two casts should have different syntaxes — I think the new one should be the "default", but I can just tell colleagues

Paolo Giarrusso (Apr 09 2021 at 16:58):

if it can be implemented in Coq itself, great, but I feel that it belongs in the stdlib and the manual...

gallais (Apr 09 2021 at 17:59):

Pierre-Marie Pédrot said:

you lose the typing constraint

I'm not sure I understand what you mean. If you put the wrong type annotation there (e.g. list nat) you do get an error. So there is some checking.

Pierre-Marie Pédrot (Apr 09 2021 at 22:47):

What I mean is that the type of the term is first inferred without any use of the type cast, and then the result is checked for convertibility with the cast.

Pierre-Marie Pédrot (Apr 09 2021 at 22:48):

This is not what is asked in this thread, i.e. the type cast needs to be taken into account in the inference phase (e.g. to help resolving typeclasses and whatnot)

gallais (Apr 09 2021 at 23:51):

I see. I guess I don't know enough about Coq's internals to have a good feeling for what is going to work or not. Even with inference first, I would assume I'd get some evars if the problem is under-constrained and these would then be solved by unification when checking against the constraint.

Matthieu Sozeau (Apr 10 2021 at 12:57):

@gallais yes, that would work, the only issue here is that you can't get a "partial term" or even an surface one to be passed to the tactic

Last updated: Oct 13 2024 at 01:02 UTC