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.
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.