Stream: Elpi users & devs

Topic: mlock Implicits

Gordon Stewart (Feb 27 2022 at 16:25):

The following works great now (thanks!):

  mlock Definition x {T:Type} (t : T) : T := t.
  Check x 1.

but I'm a bit surprised that this variant fails:

  mlock Definition y : forall {T:Type}, T -> T := fun _ x => x.
  Fail Check y 1. (*<-- I'd expect this to work.*)
  Check y _ 1.

Is that behavior intended?

Paolo Giarrusso (Feb 27 2022 at 17:15):

even without mlock, I'd think that one will fail , @Gordon Stewart — and it'll give a warning: implicit status is not part of types (unlike Agda).

Gordon Stewart (Feb 27 2022 at 19:59):

The following seems to work fine:

  Definition y : forall {T:Type}, T -> T := fun _ x => x.
  Check y 1.

and About y gives:

y is not universe polymorphic
Arguments y {T}%type_scope _
y is transparent
Expands to: Constant test.y

I suspect the implicits info is there somewhere?

Paolo Giarrusso (Feb 27 2022 at 22:08):

Sorry, you're completely right! What confused me (and probably complicates things) is the same point: a Coq first-class Type doesn't contain the implicits, so Definition must be using a non-compositional special case:

Definition foo := forall {T:Type}, T -> T.
(*
Ignoring implicit binder declaration in unexpected position.
[unexpected-implicit-declaration,syntax]
*)
Definition bar : foo := λ _ x, x.
Fail Check bar 1.
Check bar _ 1.

Paolo Giarrusso (Feb 27 2022 at 22:08):

(BTW, this isn't covered by https://coq.inria.fr/refman/language/core/definitions.html#coq:cmd.Definition, IMHO)

Enrico Tassi (Feb 27 2022 at 22:28):

I made the choice to only have the implicit status info on what I call "parameters" ( the things before the : ).

Enrico Tassi (Feb 27 2022 at 22:29):

It is a trade-off, fewer ast nodes vs completeness.

Paolo Giarrusso (Feb 27 2022 at 22:35):

If you stick to that choice, can you add the unexpected-implicit-declaration warning here too?

Enrico Tassi (Feb 28 2022 at 08:45):

Hum, right, an issue on GH would be welcome.

FTR the reason is that coq has many ASTs even for terms, some of them carry this info everywhere, but the system only understands it in a few places. In elpi I wanted to have just one, possibly wrapped.

Paolo Giarrusso (Feb 28 2022 at 09:39):

Filed https://github.com/LPCIC/coq-elpi/issues/342. And I'm a fan of dropping features that might not carry their weight.

Gordon Stewart (Feb 28 2022 at 14:32):

For context:
I have some tooling around interfaces for locked things. So, for example, you can write

Module Type INTERFACE.
  mlock Axiom x : forall {T:Type}, T -> T.
  (*Issue I'm trying to solve: need to redeclare x's implicits here.*)
  Arguments x {_} _.
  ...
  (*Further uses of x*)
  ...
End INTERFACE.

Module Implementation <: INTERFACE.
  mlock Definition x {T:Type} (t : T) := t.
  (*x's implicits correctly declared*)
  ...
End Implementation.

I raised the question because of the issue I highlight above, that people have to redeclare the implicits of Axiom x within the module type interface. It's just an annoyance, but something I was hoping to fix.

[NOTE: It may seem strange that we use transparent ascription + module locking within modules. Why is a long story, but there's a good reason.]

Enrico Tassi (Feb 28 2022 at 14:39):

I see, so isn't the real problem that Axiom f {T} : T -> T is not valid syntax? (it is easy to add to Coq and/or Elpi)

Gordon Stewart (Feb 28 2022 at 14:39):

Yes :-) I'd much prefer to be able to write Axiom f {T} : T -> T.

Gordon Stewart (Feb 28 2022 at 14:40):

Coq doesn't support that syntax currently, though, right? Are there plans to add it?

Enrico Tassi (Feb 28 2022 at 14:40):

IIRC there is a silly conflict, you can probably write Axiom x y : nat, and IIRC we added a warning that you should really write Axioms in that case

Gordon Stewart (Feb 28 2022 at 14:42):

it is easy to add to Coq and/or Elpi

Are there any issues tracking this, or concrete plans to add support to Coq that you could point me to?

Enrico Tassi (Feb 28 2022 at 14:42):

if the warning becomes an error, then we can support the nice syntax with implicits in Axiom. Let me ping @Théo Zimmermann which was involved in the discussion IIRC. I can't find anything in the changelog though...

Gordon Stewart (Feb 28 2022 at 14:43):

OK. I appreciate it. Syntax for, e.g., Axiom f {T} : T -> T would be a nice improvement.

Théo Zimmermann (Feb 28 2022 at 14:59):

Nothing is planned to change yet. See https://github.com/coq/coq/issues/15573 and https://github.com/coq/coq/pull/13416. Feel free to push for this.

Last updated: Oct 13 2024 at 01:02 UTC