The Coq mailing list

[Ben Sherman <sherman AT csail.mit.edu>]

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