Overloading notation for different types in Coq

Question

I would like to be able to define the same Coq notations for different inductive definitions, and distinguish the notations based on the types of their arguments.

Here is a minimal example:

Inductive type : Type :=
| TBool : type.

Inductive term1 : Type :=
| tvar1 : term1.

Inductive term2 : Type :=
| tvar2 : term2.

Definition context := nat -> (option type).

Reserved Notation "G '⊢' t '::' T" (at level 40, t at level 59).

Inductive typing1 : context -> term1 -> type -> Prop :=
 | T_Var1 : forall G T,
      G ⊢ tvar1 :: T
where "G '⊢' t1 '::' T" := (typing1 G t1 T)                            
with typing2 : context -> term2 -> type -> Prop :=
 | T_Var2 : forall G T,
      G ⊢ tvar2 :: T
where "G '⊢' t2 '::' T" := (typing2 G t2 T).

As you see, there is a mutually inductive definition, in which I'd like to be able to use the same notation for different types of terms (term1 and term2).

The error I get when trying to compile this is The term "tvar1" has type "term1" while it is expected to have type "term2"..

Is there a way to get this to work?

You can use notation scopes, however not sure if that will work with a where clause. — ejgallego
I would like to be able to use both meanings of the same notation throughout my proof, without having to specify scopes, if possible. — amaurremi
So how is Coq supposed to disambiguate it? There may be technical workarounds with Coercions and/or type classes, but I would just use a different turn-style for each and I would be done with it. — ejgallego
Unless you really have an injection from one to the other, etc... YMMV, it is hard to say more without having a bit more of context. One of the most generic thing you could implement would be in the style of math-comp by hacking unification and Canonicals. — ejgallego
You get this error because you try to apply tvar1 to x. This error does not report a notation problem. — eponier

amaurremi amaurremi · Accepted Answer · 2017-05-18T20:47:46

I wrote to the Coq mailing list and received an answer from Gaëtan Gilbert that solved my problem using type classes:

Inductive type : Type :=
| TBool : type.

Inductive term1 : Type :=
| tvar1 : term1.

Inductive term2 : Type :=
| tvar2 : term2.

Definition context := nat -> (option type).

Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.
Notation "G '⊢' t '::' T" := (vdash G t T) (at level 40, t at level 59).

Inductive typing1 : VDash context term1 type :=
| T_Var1 : forall G T,
    G ⊢ tvar1 :: T

with typing2 : VDash context term2 type :=
| T_Var2 : forall G T,
    G ⊢ tvar2 :: T.

Overloading notation for different types in Coq

1 Answers