[test] Add ambiguity tests

test/Scope/Negative.hs

@@ -106,4 +106,9 @@ tests = [
    "WrongModuleName.mjuvix" $ \case
       ErrWrongTopModuleName {} -> Nothing
       _ -> wrongError
+  ,  NegTest "Ambiguous export"
+    "."
+   "AmbiguousExport.mjuvix" $ \case
+      ErrMultipleExport {} -> Nothing
+      _ -> wrongError
   ]

test/Scope/Positive.hs

@@ -79,4 +79,10 @@ tests = [
      "." "Axiom.mjuvix"
   , PosTest "Foreign block parsing"
      "." "Foreign.mjuvix"
+  , PosTest "Multiple modules non-ambiguous symbol - same file"
+     "QualifiedSymbol" "M.mjuvix"
+  , PosTest "Multiple modules non-ambiguous symbol"
+     "QualifiedSymbol2" "N.mjuvix"
+  , PosTest "Multiple modules constructor non-ambiguous symbol"
+     "QualifiedConstructor" "M.mjuvix"
  ]

tests/negative/AmbiguousExport.mjuvix

@@ -0,0 +1,16 @@
+module AmbiguousExport;
+
+  module N;
+    module O;
+      inductive T {
+        A : T;
+      };
+    end;
+  end;
+
+  open N public;
+
+  module O;
+    axiom A : Type;
+  end;
+end;

tests/positive/QualifiedConstructor/M.mjuvix

@@ -0,0 +1,22 @@
+module M;
+
+  module N;
+    module O;
+      inductive T {
+        A : T;
+      };
+    end;
+  end;
+
+  open N;
+  open O using { T; A };
+
+  module O;
+    axiom A : Type;
+  end;
+
+  open O;
+
+  fun : T → T;
+  fun A ≔ T;
+end;

tests/positive/QualifiedSymbol/M.mjuvix

@@ -0,0 +1,14 @@
+module M;
+
+  module N;
+    module O;
+      axiom A : Type;
+    end;
+  end;
+  open N;
+
+  module O;
+  end;
+
+  axiom B : O.A;
+end;

tests/positive/QualifiedSymbol2/M.mjuvix

@@ -0,0 +1,3 @@
+module M;
+
+end;

tests/positive/QualifiedSymbol2/N.mjuvix

@@ -0,0 +1,10 @@
+module N;
+  import M;
+
+  module M;
+    axiom A : Type;
+  end;
+
+  axiom B : M.A;
+
+end;