The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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