[ fix #4959 ] rip out TopLevelInteraction (unfix #4647)

This commit unfixes #4647 by removing the
`InteractionMode` (`TopLevelInteraction`/`RegularInteraction`) and the
option to switch off the logic (which didn't fully work).

For #4647 there is a simple workaround: add a hole to the file so that
the interface is not serialize and thus the private definitions are
not removed.

src/full/Agda/Interaction/Base.hs

@@ -56,10 +56,6 @@ data CommandState = CommandState
     --
     -- This queue should only be manipulated by
     -- 'initialiseCommandQueue' and 'maybeAbort'.
-  , interactionMode      :: !InteractionMode
-    -- ^ For top-level commands, we switch into a mode
-    --   where the interface contains also the private definitions.
-    --   See issues #4647 and #1804.
   }
 
 type OldInteractionScopes = Map InteractionId ScopeInfo
@@ -74,7 +70,6 @@ initCommandState commandQueue =
     , optionsOnReload      = defaultOptions
     , oldInteractionScopes = Map.empty
     , commandQueue         = commandQueue
-    , interactionMode      = RegularInteraction
     }
 
 -- | Monad for computing answers to interactive commands.
@@ -93,27 +88,6 @@ data CurrentFile = CurrentFile
       -- ^ The modification time stamp of the file when it was loaded.
   } deriving (Show)
 
-------------------------------------------------------------------------
--- Interaction modes (issue #4647)
-
--- | When a command is invoked at top-level, we wish to be the scope
---   of the top-level module but also have access to the private
---   declaration that are removed during serialization.
---
---   Thus, top-level commands switch to mode 'TopLevelInteraction'
---   which initially reloads the current module to restore the
---   private declarations into the scope.
---
---   Switching to a new file will fall back to 'RegularInteraction'.
-
-data InteractionMode
-  = RegularInteraction
-      -- ^ Initial mode. Use deserialized interface.
-  | TopLevelInteraction
-      -- ^ Mode for top-level commands.  Use original interface
-      --   that also contains the private declarations.
-  deriving (Show, Eq)
-
 ------------------------------------------------------------------------
 -- Command queues
 

src/full/Agda/Interaction/BasicOps.hs

@@ -1275,8 +1275,6 @@ whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
 whyInScope s = do
   x     <- parseName noRange s
   scope <- getScope
-  ifNull ( lookup x $ map (first C.QName) $ scope ^. scopeLocals
+  return ( lookup x $ map (first C.QName) $ scope ^. scopeLocals
          , scopeLookup x scope
          , scopeLookup x scope )
-    {-then-} (notInScopeError x)  -- Andreas, 2020-05-15, issue #4647 throw error to trigger TopLevelInteraction
-    {-else-} return

src/full/Agda/Interaction/Imports.hs

@@ -4,7 +4,7 @@
     interface files.
 -}
 module Agda.Interaction.Imports
-  ( Mode, Mode', pattern ScopeCheck, pattern TypeCheck
+  ( Mode, pattern ScopeCheck, pattern TypeCheck
 
   , CheckResult (CheckResult)
   , crModuleInfo
@@ -72,7 +72,6 @@ import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 
 import Agda.TheTypeChecker
 
-import Agda.Interaction.Base     ( InteractionMode(..) )
 import Agda.Interaction.BasicOps ( getGoals, showGoals )
 import Agda.Interaction.FindFile
 import Agda.Interaction.Highlighting.Generate
@@ -161,14 +160,10 @@ setOptionsFromSourcePragmas src =
 -- | Is the aim to type-check the top-level module, or only to
 -- scope-check it?
 
-data Mode' a
+data Mode
   = ScopeCheck
-  | TypeCheck a
-  deriving (Eq, Show, Functor, Foldable)
-
-type Mode = Mode' InteractionMode
-      -- ^ Depending on the 'InteractionMode' private declaration may be retained
-      --   in the interface.
+  | TypeCheck
+  deriving (Eq, Show)
 
 -- | Are we loading the interface for the user-loaded file
 --   or for an import?
@@ -192,8 +187,7 @@ includeStateChanges NotMainInterface  = False
 -- | The kind of interface produced by 'createInterface'
 moduleCheckMode :: MainInterface -> ModuleCheckMode
 moduleCheckMode = \case
-    MainInterface (TypeCheck TopLevelInteraction) -> ModuleTypeCheckedRetainingPrivates
-    MainInterface (TypeCheck RegularInteraction)  -> ModuleTypeChecked
+    MainInterface TypeCheck                       -> ModuleTypeChecked
     NotMainInterface                              -> ModuleTypeChecked
     MainInterface ScopeCheck                      -> ModuleScopeChecked
 
@@ -288,12 +282,7 @@ alreadyVisited :: C.TopLevelModuleName ->
                   TCM ModuleInfo
 alreadyVisited x isMain currentOptions getModule =
   case isMain of
-    -- Andreas, 2020-05-13, issue 4647:
-    -- For top-level interaction commands, we may not able to reuse
-    -- the existing interface, since it does not contain the private
-    -- declarations.  Thus, we always recheck.
-    MainInterface (TypeCheck TopLevelInteraction) ->              loadAndRecordVisited -- ModuleTypeCheckedRetainingPrivates
-    MainInterface (TypeCheck RegularInteraction)  -> useExistingOrLoadAndRecordVisited ModuleTypeChecked
+    MainInterface TypeCheck                       -> useExistingOrLoadAndRecordVisited ModuleTypeChecked
     NotMainInterface                              -> useExistingOrLoadAndRecordVisited ModuleTypeChecked
     MainInterface ScopeCheck                      -> useExistingOrLoadAndRecordVisited ModuleScopeChecked
   where
@@ -485,8 +474,6 @@ getInterface x isMain msrc =
       -- Andreas, 2015-07-13: Serialize iInsideScope again.
       -- Andreas, 2020-05-13 issue #4647: don't skip if reload because of top-level command
       stored <- runExceptT $ Bench.billTo [Bench.Import] $ do
-        when (isMain == MainInterface (TypeCheck TopLevelInteraction)) $
-          throwError "we always re-check the main interface in top-level interaction"
         getStoredInterface x file msrc
 
       let recheck = \reason -> do
@@ -1097,16 +1084,6 @@ createInterface mname file isMain msrc = do
       ([], MainInterface ScopeCheck) -> do
         reportSLn "import.iface.create" 7 "We are just scope-checking, skipping writing interface file."
         return i
-      ([], MainInterface (TypeCheck TopLevelInteraction)) -> do
-        -- -- suggested by unclebetty at https://github.com/agda/agda/issues/4959#issuecomment-706179266
-        -- reportSLn "import.iface.create" 7 $ unlines
-        --   [ "We are in top-level interaction mode and want to retain private declarations."
-        --   , "We write the interface file but retain the private declarations."
-        --   ]
-        -- ifile <- toIFile file
-        -- _serializedIface <- writeInterface ifile i
-        reportSLn "import.iface.create" 7 "We are in top-level interaction mode and want to retain private declarations, skipping writing interface file."
-        return i
       ([], _) -> Bench.billTo [Bench.Serialization] $ do
         reportSLn "import.iface.create" 7 "Actually calling writeInterface."
         -- The file was successfully type-checked (and no warnings were

src/full/Agda/Interaction/InteractionTop.hs

@@ -60,7 +60,7 @@ import Agda.Interaction.Response hiding (Function, ExtendedLambda)
 import qualified Agda.Interaction.Response as R
 import qualified Agda.Interaction.BasicOps as B
 import Agda.Interaction.Highlighting.Precise hiding (Error, Postulate, singleton)
-import Agda.Interaction.Imports  ( Mode, Mode', pattern ScopeCheck, pattern TypeCheck )
+import Agda.Interaction.Imports  ( Mode, pattern ScopeCheck, pattern TypeCheck )
 import qualified Agda.Interaction.Imports as Imp
 import Agda.Interaction.Highlighting.Generate
 
@@ -76,7 +76,7 @@ import Agda.Utils.Lens
 import qualified Agda.Utils.Maybe.Strict as Strict
 import Agda.Utils.Monad
 import Agda.Utils.Null
-import Agda.Utils.Pretty
+import Agda.Utils.Pretty hiding (Mode)
 import Agda.Utils.Singleton
 import Agda.Utils.String
 import Agda.Utils.Time
@@ -283,7 +283,7 @@ runInteraction (IOTCM current highlighting highlightingMethod cmd) =
     -- loaded.
     cf <- gets theCurrentFile
     when (not (independent cmd) && Just currentAbs /= (currentFilePath <$> cf)) $ do
-        let mode = TypeCheck Nothing
+        let mode = TypeCheck
         cmd_load' current [] True mode $ \_ -> return ()
 
     withCurrentFile $ interpret cmd
@@ -496,7 +496,7 @@ interpret :: Interaction -> CommandM ()
 interpret (Cmd_load m argv) =
   cmd_load' m argv True mode $ \_ -> interpret $ Cmd_metas AsIs
   where
-  mode = TypeCheck Nothing -- do not reset InteractionMode
+  mode = TypeCheck
 
 interpret (Cmd_compile backend file argv) =
   cmd_load' file argv allowUnsolved mode $ \ checkResult -> do
@@ -513,7 +513,7 @@ interpret (Cmd_compile backend file argv) =
   where
   allowUnsolved = backend `elem` [LaTeX, QuickLaTeX]
   mode | QuickLaTeX <- backend = ScopeCheck
-       | otherwise             = TypeCheck $ Just RegularInteraction  -- reset InteractionMode
+       | otherwise             = TypeCheck
 
 interpret Cmd_constraints =
     display_info . Info_Constraints =<< lift B.getConstraints
@@ -869,36 +869,16 @@ cmd_load'
   :: FilePath  -- ^ File to load into interaction.
   -> [String]  -- ^ Arguments to Agda for loading this file
   -> Bool      -- ^ Allow unsolved meta-variables?
-  -> Mode' (Maybe InteractionMode)
-               -- ^ Full type-checking, or only scope-checking?
-               --   Providing 'TypeCheck (Just mode)' here
-               --   will reset 'InteractionMode' accordingly.
-               --   Otherwise, reset to 'RegularInteraction'
-               --   only if different file from last time.
+  -> Mode      -- ^ Full type-checking, or only scope-checking?
   -> (CheckResult -> CommandM a)
                -- ^ Continuation after successful loading.
   -> CommandM a
-cmd_load' file argv unsolvedOK modeChange cmd = do
+cmd_load' file argv unsolvedOK mode cmd = do
     fp <- liftIO $ absolute file
     ex <- liftIO $ doesFileExist $ filePath fp
     unless ex $ typeError $ GenericError $
       "The file " ++ file ++ " was not found."
 
-    -- When switching to a new file, or @modeChange@ indicates such a reset,
-    -- fall back to RegularInteraction.
-    mode <- do
-      let typeCheckMode m = TypeCheck m <$ setInteractionMode m
-      case modeChange of
-        ScopeCheck               -> pure ScopeCheck
-        TypeCheck (Just newmode) -> typeCheckMode newmode
-        TypeCheck Nothing        -> do
-          -- If the file has not changed, keep the existing mode, otherwise
-          -- use 'RegularInteraction' mode.
-          gets theCurrentFile >>= \case
-            Just CurrentFile{ currentFilePath = fp' } | fp == fp'
-              -> TypeCheck <$> gets interactionMode
-            _ -> typeCheckMode RegularInteraction
-
     -- Forget the previous "current file" and interaction points.
     modify $ \ st -> st { theInteractionPoints = []
                         , theCurrentFile       = Nothing
@@ -960,47 +940,14 @@ cmd_load' file argv unsolvedOK modeChange cmd = do
 
     cmd ok
 
-  where
-  -- Update import mode to RegularInteraction.
-  regularMode = \case
-    TypeCheck _ -> TypeCheck RegularInteraction
-    ScopeCheck  -> ScopeCheck
-
 -- | Set 'envCurrentPath' to 'theCurrentFile', if any.
 withCurrentFile :: CommandM a -> CommandM a
 withCurrentFile m = do
   mfile <- gets $ fmap currentFilePath . theCurrentFile
   localTC (\ e -> e { envCurrentPath = mfile }) m
 
--- | Top-level commands switch to 'TopLevelInteraction' mode if necessary.
 atTopLevel :: CommandM a -> CommandM a
-atTopLevel cmd = do
-  -- Don't switch if --top-level-interaction-no-private.
-  ifM (optTopLevelInteractionNoPrivate <$> pragmaOptions) continue $ {-else-} do
-  gets interactionMode >>= \case
-    TopLevelInteraction -> continue  -- Already in the correct mode.
-    RegularInteraction  -> continue `handleNotInScope` do
-      -- Have to switch mode.
-      CurrentFile file argv _stamp <- gets $ fromMaybe __IMPOSSIBLE__ . theCurrentFile
-      let allowUnsolved = True
-          mode          = TypeCheck $ Just TopLevelInteraction
-      cmd_load' (filePath file) argv allowUnsolved mode $ \ _ -> continue
-  where
-  continue      = liftCommandMT B.atTopLevel cmd
-
-setInteractionMode :: InteractionMode -> CommandM ()
-setInteractionMode mode = modify $ \ st -> st { interactionMode = mode }
-
--- | Handle a 'NotInScope' error, reraise other errors.
-handleNotInScope :: CommandM a -> CommandM a -> CommandM a
-handleNotInScope cmd handler = do
-  cmd `catchError` \case
-    TypeError _ _ (Closure _sig _env _scope _checkpoints (TCM.NotInScope _xs)) -> do
-      reportSLn "interaction.top" 60 $ "Handling `Not in scope` error"
-      handler
-    err -> do
-      reportSLn "interaction.top" 60 $ show err
-      throwError err
+atTopLevel cmd = liftCommandMT B.atTopLevel cmd
 
 ---------------------------------------------------------------------------
 -- Giving, refining.

src/full/Agda/Interaction/Options/Base.hs

@@ -165,10 +165,6 @@ data PragmaOptions = PragmaOptions
   , optKeepPatternVariables      :: Bool
       -- ^ Should case splitting replace variables with dot patterns
       --   (False) or keep them as variables (True).
-  , optTopLevelInteractionNoPrivate :: Bool
-     -- ^ If @True@, disable reloading mechanism introduced in issue #4647
-     --   that brings private declarations in main module into scope
-     --   to remedy not-in-scope errors in top-level interaction commands.
   , optInstanceSearchDepth       :: Int
   , optOverlappingInstances      :: Bool
   , optQualifiedInstances        :: Bool  -- ^ Should instance search consider instances with qualified names?
@@ -295,7 +291,6 @@ defaultPragmaOptions = PragmaOptions
   , optFirstOrder                = False
   , optPostfixProjections        = False
   , optKeepPatternVariables      = False
-  , optTopLevelInteractionNoPrivate = False
   , optInstanceSearchDepth       = 500
   , optOverlappingInstances      = False
   , optQualifiedInstances        = True
@@ -721,9 +716,6 @@ postfixProjectionsFlag o = return $ o { optPostfixProjections = True }
 keepPatternVariablesFlag :: Flag PragmaOptions
 keepPatternVariablesFlag o = return $ o { optKeepPatternVariables = True }
 
-topLevelInteractionNoPrivateFlag :: Flag PragmaOptions
-topLevelInteractionNoPrivateFlag o = return $ o { optTopLevelInteractionNoPrivate = True }
-
 instanceDepthFlag :: String -> Flag PragmaOptions
 instanceDepthFlag s o = do
   d <- integerArgument "--instance-search-depth" s
@@ -981,8 +973,6 @@ pragmaOptions =
                     "make postfix projection notation the default"
     , Option []     ["keep-pattern-variables"] (NoArg keepPatternVariablesFlag)
                     "don't replace variables with dot patterns during case splitting"
-    , Option []     ["top-level-interaction-no-private"] (NoArg topLevelInteractionNoPrivateFlag)
-                    "in top-level interaction commands, don't reload file to bring private declarations into scope"
     , Option []     ["instance-search-depth"] (ReqArg instanceDepthFlag "N")
                     "set instance search depth to N (default: 500)"
     , Option []     ["overlapping-instances"] (NoArg overlappingInstancesFlag)

src/full/Agda/Main.hs

@@ -15,7 +15,6 @@ import System.Console.GetOpt
 
 import Paths_Agda            ( getDataDir )
 
-import Agda.Interaction.Base ( pattern RegularInteraction )
 import Agda.Interaction.CommandLine
 import Agda.Interaction.ExitCode (AgdaError(..), exitSuccess, exitAgdaWith)
 import Agda.Interaction.Options
@@ -200,7 +199,7 @@ runAgdaWithOptions interactor progName opts = do
         -- resetState
           let mode = if optOnlyScopeChecking opts
                      then Imp.ScopeCheck
-                     else Imp.TypeCheck RegularInteraction
+                     else Imp.TypeCheck
 
           result <- Imp.typeCheckMain mode =<< Imp.parseSource (SourceFile inputFile)
 

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -893,7 +893,6 @@ instance MonadStConcreteNames m => MonadStConcreteNames (StateT s m) where
 data ModuleCheckMode
   = ModuleScopeChecked
   | ModuleTypeChecked
-  | ModuleTypeCheckedRetainingPrivates
   deriving (Eq, Ord, Bounded, Enum, Show, Generic)
 
 

src/full/Agda/TypeChecking/Monad/Imports.hs

@@ -72,7 +72,6 @@ getPrettyVisitedModules = do
   where
   prettyCheckMode :: ModuleCheckMode -> Doc
   prettyCheckMode ModuleTypeChecked                  = ""
-  prettyCheckMode ModuleTypeCheckedRetainingPrivates = " (+ privates)"
   prettyCheckMode ModuleScopeChecked                 = " (scope only)"
 
 getVisitedModule :: ReadTCState m

src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs

@@ -267,12 +267,12 @@ instance EmbPrj Doc where
 
 instance EmbPrj PragmaOptions where
   icod_ = \case
-    PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd ->
-      icodeN' PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd
+    PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ->
+      icodeN' PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc
 
   value = vcase $ \case
-    [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, bb, cc, dd, ee, ff, gg, hh, ii, jj, kk, ll, mm, nn, oo, pp, qq, rr, ss, tt, uu, vv, ww, xx, yy, zz, aaa, bbb, ccc, ddd] ->
-      valuN PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd
+    [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, bb, cc, dd, ee, ff, gg, hh, ii, jj, kk, ll, mm, nn, oo, pp, qq, rr, ss, tt, uu, vv, ww, xx, yy, zz, aaa, bbb, ccc] ->
+      valuN PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc
     _ -> malformed
 
 instance EmbPrj UnicodeOrAscii

test/interaction/Issue1804.out

@@ -4,8 +4,5 @@
 (agda2-status-action "Checked")
 (agda2-info-action "*All Done*" "" nil)
 ((last . 1) . (agda2-goals-action '()))
-(agda2-status-action "")
-(agda2-info-action "*Type-checking*" "" nil)
-(agda2-highlight-clear)
 (agda2-status-action "Checked")
-(agda2-info-action "*Scope Info*" "F is in scope as * a record field Issue1804._.F brought into scope by - the application of R at Issue1804.agda:8,6-7 - its definition at Issue1804.agda:4,9-10" nil)
+(agda2-info-action "*Scope Info*" "F is not in scope." nil)

test/interaction/Long.out

@@ -91,9 +91,6 @@
 (agda2-info-action "*Inferred Type*" "Maybe Nat" nil)
 (agda2-status-action "")
 (agda2-info-action "*Normal Form*" "Nothing" nil)
-(agda2-status-action "")
-(agda2-info-action "*Type-checking*" "" nil)
-(agda2-highlight-clear)
 (agda2-info-action "*Error*" "1,4-5 Not in scope: n at 1,4-5 when scope checking n" nil)
 (agda2-highlight-load-and-delete-action)
 (agda2-status-action "")