agda#6972: Also save backcopies in interface file (agda#6974)

src/full/Agda/Interaction/Imports.hs

@@ -1257,7 +1257,9 @@ buildInterface src topLevel = do
     let
       mh = moduleNameId (srcModuleName src)
       opaqueBlocks = Map.filterWithKey (\(OpaqueId _ mod) _ -> mod == mh) opaqueBlocks'
-      opaqueIds    = Map.filterWithKey (\_ (OpaqueId _ mod) -> mod == mh) opaqueIds'
+      isLocal qnm = case nameId (qnameName qnm) of
+        NameId _ mh' -> mh' == mh
+      opaqueIds = Map.filterWithKey (\qnm (OpaqueId _ mod) -> isLocal qnm || mod == mh) opaqueIds'
 
     -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
     -- serialization to avoid error locations pointing to external files

src/full/Agda/TypeChecking/Opacity.hs

@@ -58,7 +58,6 @@ saturateOpaqueBlocks moddecs = entry where
       canonise name = fromMaybe name (HashMap.lookup name canonical)
       ours = snd <$> filter isOurs (Map.toAscList known)
 
-    unless (null ours) $ do
     () <- liftIO $ evaluate (rnf (canonical, backcopies))
 
     reportSDoc "tc.opaque" 30 $ vcat $

test/Succeed/Issue6972a.agda

@@ -0,0 +1,5 @@
+module Issue6972a (A : Set₁) where
+
+opaque
+  B : Set₁
+  B = A

test/Succeed/Issue6972b.agda

@@ -0,0 +1,3 @@
+module Issue6972b (A : Set₁) where
+
+open import Issue6972a A public

test/Succeed/Issue6972c.agda

@@ -0,0 +1,11 @@
+module Issue6972c where
+
+open import Agda.Builtin.Equality
+
+open import Issue6972b Set
+
+opaque
+  unfolding B
+
+  _ : B ≡ Set
+  _ = refl