coq

Coq notation defined inside a module expecting type without module prefix

I'm writing a compiler and its proof for a toy language, and I have files L1, L2, C, and P, where L1 and L2 contain the abstract syntax and operational semantics of languages l1 and l2, C containing the compiler, and P containing the proof. Some definitions in L1 have the same name as definitions in L2, like the types "heap", "program", etc.

To avoid name conflict, I put everything in L1 inside a module named A, so that in files C and P I can refer to the types in L1 as "A.name" while the type of L2 with same name is just "name". In module A I defined a notation expecting a type X. When I use it in P, I get error message saying that it expects type X while I gave it type A.X.

File L1 looks like this:

From Coq Require Import Lists.List. Import ListNotations.
From Coq Require Import Strings.String.
Declare Scope L1_scope.
Open Scope L1_scope.
Module A.
...
Notation "'_' '!->h' v" := (h_empty v)
(at level 100, right associativity):L1_scope.
...
End A.
Close Scope L1_scope.

File P looks like this:

From L Require Import L1.
From L Require Import L2.
From L Require Import C.
Open Scope L1_scope
(... inside some definition ...): _ !->h tm

Error message looks like this:

In environment
...
The term "tm"
has type "A.X"
while it is expected to have type
"X".

Also as a side question, is there an idiomatic way of resolving name conflicts in a situation like this that doesn't require me to write too much code? I didn't put definitions in L2 in another module because that would make all names really long and cumbersome to refer to.

Solution

  • Here is an attempt at building an minimal reproducing example.

    Exact contents of file L1:

    From Coq Require Import Lists.List. Import ListNotations.
From Coq Require Import Strings.String.
Declare Scope L1_scope.
Open Scope L1_scope.

Module A.

Definition X := list nat.
Definition h_empty (v : X) := (v = nil).

Notation "'_' '!->h' v" := (h_empty v)
(at level 100, right associativity):L1_scope.

End A.

Close Scope L1_scope.

    Exact content of file P.

    Require Import L1.

Import A.

Open Scope L1_scope.

Check (fun tm : A.X => _ !->h tm).

    If I don't include the line Import A. then the notation is not recognized. If I do import A, the Check always succeeds, whether tm is declared as having type X or type A.X.

    So with the question as it is given now, we are not able to reproduce the problem. Provide us with YOUR minimal reproducible example.