The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Making the notation only parsing doesn't change anything.

I think Coq is lying to you.  If you change the notation to:

  Notation "[ e ]" := (let v := Build_WfTerm (fun _ => e) (undefined _) in let dummy : True := ltac:(proveWF) in v) (only parsing).

you later get the error (with [Set Printing All]):

Error: Cannot infer the implicit parameter var of Const whose type is

"forall _ : bool, Type" in environment:

A : bool

v := @Build_WfTerm A (fun var : forall _ : bool, Type => @Const var A) (undefined True) : WfTerm A

I think what happens here is that Coq tries to reinterpret all of the notation's arguments in the Ltac context without any typing information (so that you can use them in the tactic, if you want).  Pierre-Marie can probably explain what exactly goes wrong, or why Coq does this.

File a bug?  Perhaps related: https://coq.inria.fr/bugs/show_bug.cgi?id=4728

On Mon, Jul 4, 2016 at 2:02 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

In general, one should not mix tactic-in-term with notations, unless the
notations are "only parsing".

See https://coq.inria.fr/bugs/show_bug.cgi?id=4595


-- Jonathan


On 07/04/2016 04:57 PM, Ben Sherman wrote:
> Hi all,
>
> My general understanding of Coq notations is that they first are "desugared" and then the resulting term is interpreted (including inference and ltac-in-term). However, I cannot explain the following behavior, where a tactic-in-term in notation breaks inference:
>
>> Inductive term {var : bool -> Type} : bool -> Type :=
>>    | Var : forall A : bool, var A -> term A
>>    | Const : forall A : bool, term A.
>>
>> Arguments term : clear implicits.
>>
>> Record WfTerm {A} :=
>>    { WfT_Term : forall var, term var A
>>    ; WfT_Ok : True
>>    }.
>>
>> Arguments WfTerm : clear implicits.
>> Arguments Build_WfTerm {A} _ _.
>>
>> Axiom undefined : forall A, A.
>>
>> Ltac proveWF := exact (undefined _).
>>
>> Notation "[ e ]" := (Build_WfTerm (fun _ => e) (ltac:(proveWF))).
>> Notation "<< e >>" := (Build_WfTerm (fun _ => e) (undefined _)).
>>
>> Definition konst {A : bool} : WfTerm A :=
>>    Build_WfTerm (fun _ => Const A) (ltac:(proveWF)).
>>
>> Definition konst1 {A : bool} : WfTerm A :=
>>     << Const A >> .
>>
>> (* Why doesn't this work? It looks like it should just
>>    "desugar" to the definition of 'konst', and is also similar
>>    to 'konst1'. *)
>> Fail Definition konst2 {A : bool} : WfTerm A :=
>>    [ Const A ] .
>> (*
>> Cannot infer the implicit parameter var of Const whose type is
>> "bool -> Type" in environment:
>> A : bool
>> *)
> Is there some way to understand what it is about the combination of the notation and the tactic-in-term that's breaking type inference? Or is it possible that this is a bug?
>
> Thanks,
> Ben