Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip 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!)

view this post on Zulip Enrico Tassi (Apr 09 2021 at 13:19):

Does SSR's rewrite have this problem too?

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 13:20):

not sure but I expect yes

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 13:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 13:23):

it should be removed after inference

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:24):

Won't you have issues during Qed then?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 13:24):

this is not in the proof but in statements

view this post on Zulip Michael Soegtrop (Apr 09 2021 at 13:24):

Ah ok, I see.

view this post on Zulip 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/...

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2021 at 14:25):

define "comparing"

view this post on Zulip 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)

view this post on Zulip Meven Lennon-Bertrand (Apr 09 2021 at 14:26):

Ah, that is what I meant

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2021 at 14:28):

because term equality is far to be pattern recognition

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2021 at 14:29):

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

view this post on Zulip Meven Lennon-Bertrand (Apr 09 2021 at 14:29):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2021 at 14:29):

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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2021 at 14:31):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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: Jan 28 2023 at 07:30 UTC