Fix agda#6729: clear loneSigs before inferring mutual blocks in an op…

…aque block.
JobPetrovcic · Apr 12, 2024 · 3b26a97 · 3b26a97
1 parent 88bb4f0
commit 3b26a97
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 1 deletion.
diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs
@@ -531,7 +531,11 @@ niceDeclarations fixs ds = do
           -- The body of an 'opaque' definition can have mutual
           -- recursion by interleaving type signatures and definitions,
           -- just like the body of a module.
-          body <- inferMutualBlocks =<< nice body
+          decls0 <- nice body
+          ps <- use loneSigs
+          checkLoneSigs ps
+          let decls = replaceSigs ps decls0
+          body <- inferMutualBlocks decls
           pure ([NiceOpaque r (concat unfoldings) body], ds)
 
         Unfolding r _ -> declarationException $ UnfoldingOutsideOpaque r

diff --git a/test/Fail/Issue6729.agda b/test/Fail/Issue6729.agda
@@ -0,0 +1,2 @@
+opaque
+  test : Set
diff --git a/test/Fail/Issue6729.err b/test/Fail/Issue6729.err
@@ -0,0 +1,10 @@
+Issue6729.agda:1,1-2,13
+warning: -W[no]UselessOpaque
+This 'opaque' block has no effect.
+when scope checking the declaration
+  opaque
+    unfolding {}
+    test : Set
+Issue6729.agda:2,3-7
+The following names are declared but not accompanied by a
+definition: test