Re. #7196: Only prune instances in serialised iface (#7197)

src/full/Agda/Interaction/Imports.hs

@@ -921,7 +921,9 @@ writeInterface file i = let fp = filePath file in do
     -- [Old: Andreas, 2016-02-02 this causes issue #1804, so don't do it:]
     -- Andreas, 2020-05-13, #1804, #4647: removed private declarations
     -- only when we actually write the interface.
-    let filteredIface = i { iInsideScope  = withoutPrivates $ iInsideScope i }
+    let
+      filteredIface = i { iInsideScope = withoutPrivates $ iInsideScope i }
+    filteredIface <- pruneTemporaryInstances filteredIface
     reportSLn "import.iface.write" 50 $
       "Writing interface file with hash " ++ show (iFullHash filteredIface) ++ "."
     encodedIface <- encodeFile fp filteredIface
@@ -1058,10 +1060,6 @@ createInterface mname file isMain msrc = do
 
     unfreezeMetas
 
-    -- Remove any instances that now have visible arguments from the
-    -- instance tree before serialising.
-    pruneTemporaryInstances
-
     -- Profiling: Count number of metas.
     whenProfile Profile.Metas $ do
       m <- fresh

src/full/Agda/TypeChecking/InstanceArguments.hs

@@ -831,7 +831,8 @@ getInstanceDefs = do
     typeError $ GenericError $ "There are instances whose type is still unsolved"
   return $ fst insts
 
--- | Remove introduced in modules with visible arguments.
+-- | Prune an 'Interface' to remove any instances that would be
+-- inapplicable in child modules.
 --
 -- While in a section with visible arguments, we add any instances
 -- defined locally to the instance table: you have to be able to find
@@ -840,11 +841,15 @@ getInstanceDefs = do
 --
 -- But when we leave such a section, these instances have no more value:
 -- even though they might technically be in scope, their types are
--- malformed, since they have visible pis. This function deletes these
--- instances from the instance tree to save on serialisation time *and*
--- time spent checking for candidate validity.
-pruneTemporaryInstances :: TCM ()
-pruneTemporaryInstances = do
+-- malformed, since they have visible pis.
+--
+-- This function deletes these instances from the instance tree in the
+-- given signature to save on serialisation time *and* time spent
+-- checking for candidate validity in client modules. It can't do this
+-- directly in the TC state to prevent these instances from going out of
+-- scope before interaction (see #7196).
+pruneTemporaryInstances :: Interface -> TCM Interface
+pruneTemporaryInstances int = do
   todo <- useTC stTemporaryInstances
 
   reportSDoc "tc.instance.prune" 30 $ vcat
@@ -853,8 +858,5 @@ pruneTemporaryInstances = do
     , "todo:" <+> prettyTCM todo
     ]
 
-  modifyTCLens' (stSignature . sigInstances . itableTree) $
-    flip deleteFromDT todo
-  reportSDoc "tc.instance.prune" 60 $ prettyTCM =<< useTC (stSignature . sigInstances . itableTree)
-
-  setTCLens' stTemporaryInstances mempty
+  let sig' = over (sigInstances . itableTree) (flip deleteFromDT todo) (iSignature int)
+  pure int{ iSignature = sig' }

test/interaction/Issue7196.agda

@@ -0,0 +1,20 @@
+module Issue7196 where
+
+
+postulate
+  T : Set
+  I : T → Set
+
+record Foo : Set where
+  field
+    t : T
+    instance
+      I-t : I t
+
+auto : ∀ {ℓ} {A : Set ℓ} → ⦃ A ⦄ → A
+auto ⦃ a ⦄ = a
+
+module _ (f : Foo) where -- f needs to be visible
+  open Foo f
+  bug : I t
+  bug = {! auto !}

test/interaction/Issue7196.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_give "auto"

test/interaction/Issue7196.out

@@ -0,0 +1,10 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : I t " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-give-action 0 "auto")
+(agda2-status-action "")
+(agda2-info-action "*All Done*" "" nil)
+((last . 1) . (agda2-goals-action '()))