The Coq mailing list

[Marianna Rapoport <mrapoport AT uwaterloo.ca>]

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 x 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 `Error: Illegal application (Non-functional construction): The _expression_ "tvar1" of type "term1" cannot be applied to the term "x" : "?T"`.

Is there a way to get this to work, maybe by using type classes?