notations scopes bound to types not honoured for raw arguments

[gares]

https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/syntax.20scopes.20in.20raw.20arguments.20for.20commands

[gares]

From elpi Require Import elpi.

#[arguments(raw)] Elpi Command PrintCommand.
Elpi Accumulate lp:{{

  % main is, well, the entry point
  main Arguments :- coq.say "PrintCommand" Arguments.

}}.
Elpi Typecheck.
Elpi Export PrintCommand.

Definition siProp := nat -> Prop.

Definition f : siProp -> siProp.
Admitted.

Declare Scope siPropScope.
Delimit Scope siPropScope with S.
Bind Scope siPropScope with siProp.

About f.

Notation "'bar'" := (fun n => True) : core .
Notation "'bar'" := (f) : siPropScope .

PrintCommand
Inductive foo : nat -> siProp :=
    | test g : bar g.

[gares]

@lukovdm I'm a bit confused here. I guess you want to activate siPropScope on bar by binding the scope to the siProp type. But here I don't see where the type would be imposed on bar. If you write f (bar g) then you get f (f g) as expected, since the outer f expects a siProp hence its argument is parsed in that scope. I guess you "broke" your test case by minimizing it.

[lukovdm]

You are right, I think I fixed my test case.

From elpi Require Import elpi.

#[arguments(raw)] Elpi Command PrintCommand.
Elpi Accumulate lp:{{

  % main is, well, the entry point
  main Arguments :- coq.say "PrintCommand" Arguments.

}}.
Elpi Typecheck.
Elpi Export PrintCommand.

Definition siProp := nat -> Prop.

Definition f : siProp -> siProp.
Admitted.

Declare Scope siPropScope.
Delimit Scope siPropScope with S.
Bind Scope siPropScope with siProp.

About f.

Notation "'bar'" := (fun _ n => True) : core .
Notation "'bar'" := (f) : siPropScope .

Local Open Scope core.

PrintCommand
Inductive foo : siProp :=
    | test : bar foo.

Thus, the bar from core is taken here instead of the one from siPropScope. And when writing f (bar foo) in de inductive defintion to get coq to recognize the bound scope we do get the correct bar.

[gares]

I'm still confused. Take this example where I cut elpi out of the picture:

Definition siProp := nat -> Prop.

Definition f : siProp -> siProp.
Admitted.

Declare Scope siPropScope.
Delimit Scope siPropScope with S.
Bind Scope siPropScope with siProp.

About f.

Notation "'bar'" := (fun _ n => True) : core .
Notation "'bar'" := (f) : siPropScope .

Local Open Scope core.

Inductive foo : siProp :=
    | test : bar foo.

I get:

Error: In environment
foo : siProp
The term "(fun (H : siProp) (_ : ?T@{y:=H}) => True) foo" has type
"?T@{foo:=foo; y:=foo} -> Prop" which should be Set, Prop or Type.

So coq uses the notation from core. I don't get why you expect elpi to pick the notation from siPropScope. After all, the expected value for bar foo is siProp, while its expected type is a sort. The Bind Scope mechanisms attaches the scope to a type, and open it on terms of that expected type.