Agda 2.5.4.1 → 2.5.4.2

raw patch · 25 files changed

+428/−162 lines, 25 filesdep +filemanipdep ~textPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: filemanip

Dependency ranges changed: text

API changes (from Hackage documentation)

Files

• Agda.cabal +19/−7
• CHANGELOG.md +23/−2
• doc/user-manual.pdf binary
• src/data/emacs-mode/agda2-mode-pkg.el +1/−1
• src/data/emacs-mode/agda2-mode.el +1/−1
• src/full/Agda/Compiler/Backend.hs +2/−2
• src/full/Agda/Interaction/Imports.hs +30/−25
• src/full/Agda/Interaction/Imports.hs-boot +6/−0
• src/full/Agda/Interaction/InteractionTop.hs +2/−2
• src/full/Agda/Interaction/Options.hs +35/−18
• src/full/Agda/Interaction/Options/Warnings.hs +35/−2
• src/full/Agda/Main.hs +2/−2
• src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +2/−2
• src/full/Agda/TypeChecking/Errors.hs +25/−37
• src/full/Agda/TypeChecking/Free/Reduce.hs +117/−0
• src/full/Agda/TypeChecking/MetaVars/Occurs.hs +76/−9
• src/full/Agda/TypeChecking/Monad/Base.hs +21/−6
• src/full/Agda/TypeChecking/Serialise.hs +1/−1
• src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs +2/−1
• src/full/Agda/TypeChecking/Warnings.hs +16/−38
• stack-7.10.3.yaml +4/−0
• stack-8.0.2.yaml +1/−0
• stack-8.2.2.yaml +2/−1
• stack-8.4.3.yaml +0/−5
• stack-8.4.4.yaml +5/−0

@@ -1,5 +1,5 @@ name:            Agda-version:         2.5.4.1+version:         2.5.4.2 cabal-version:   >= 1.10 build-type:      Custom license:         OtherLicense@@ -36,7 +36,7 @@ tested-with:        GHC == 7.10.3                     GHC == 8.0.2                     GHC == 8.2.2-                    GHC == 8.4.3+                    GHC == 8.4.4 extra-source-files: CHANGELOG.md                     README.md                     doc/user-manual.pdf@@ -44,7 +44,7 @@                     stack-7.10.3.yaml                     stack-8.0.2.yaml                     stack-8.2.2.yaml-                    stack-8.4.3.yaml+                    stack-8.4.4.yaml  data-dir:           src/data data-files:         Agda.css@@ -83,10 +83,10 @@ source-repository this   type:     git   location: https://github.com/agda/agda.git-  tag:      v2.5.4.1+  tag:      v2.5.4.2  flag cpphs-  default:     True+  default:     False   manual:      True   description: Use cpphs instead of cpp. @@ -102,6 +102,8 @@     Enable the --count-clusters flag. (If enable-cluster-counting is     False, then the --count-clusters flag triggers an error message.) +-- ASR (2018-09-14). Every new setup dependency should also be added+-- as a library dependency. See Issue #3225. custom-setup   setup-depends:  base >= 4.8.0.0 && < 4.12                 , Cabal >= 1.22.5.0 && < 2.3@@ -173,7 +175,6 @@                 , stm >= 2.4.4 && < 2.5                 , strict >= 0.3.2 && < 0.4                 , template-haskell >= 2.10.0.0 && < 2.14-                , text >= 0.11.3.1 && < 1.3                 , time >= 1.5.0.1 && < 1.9                 , unordered-containers >= 0.2.5.0 && < 0.3                 , uri-encode >= 1.5.0.4 && < 1.6@@ -184,11 +185,21 @@   if impl(ghc >= 8.4)     build-depends: transformers == 0.5.5.0 +  -- ASR (2018-10-16). Required for supporting GHC 8.4.1, 8.4.2 and+  -- 8.4.3. See Issue #3277.+  if impl(ghc >= 8.4.1) && impl(ghc <= 8.4.3)+    build-depends: text >= 1.2.3.0 && < 1.3+  else+    build-depends: text >= 1.2.3.1 && < 1.3+   if impl(ghc >= 8.0) && impl(ghc < 8.4)     build-depends: transformers == 0.5.2.0 +  -- ASR (2018-09-14). We add the dependency on the filemanip library+  -- due to Issue #3225.   if impl(ghc >= 7.10) && impl(ghc < 8.0)-    build-depends: transformers == 0.4.2.0+    build-depends:   transformers == 0.4.2.0+                   , filemanip >= 0.3.6.2 && < 0.4    -- zlib >= 0.6.1 is broken with GHC < 7.10.3. See Issue 1518.   if impl(ghc < 7.10.3)@@ -359,6 +370,7 @@                     Agda.TypeChecking.Free.Lazy                     Agda.TypeChecking.Free.Old                     Agda.TypeChecking.Free.Precompute+                    Agda.TypeChecking.Free.Reduce                     Agda.TypeChecking.Forcing                     Agda.TypeChecking.Functions                     Agda.TypeChecking.Implicit

@@ -1,3 +1,26 @@+Release notes for Agda version 2.5.4.2+======================================++Installation and infrastructure+-------------------------------++* Fixed installation with some old versions of `cabal-install`+  [Issue [#3225](https://github.com/agda/agda/issues/3225)].++* Using `cpp` instead of `cpphs` as the default preprocessor+  [Issue [#3223](https://github.com/agda/agda/issues/3223)].++* Added support for GHC 8.4.4.++Other closed issues+--------------------++For 2.5.4.2 the following issues have also been closed+(see [bug tracker](https://github.com/agda/agda/issues)):++  - [#3199](https://github.com/agda/agda/issues/3199): Panics when serialising absolute paths+  - [#3312](https://github.com/agda/agda/issues/3312): Crash in Substitute.hs+ Release notes for Agda version 2.5.4.1 ====================================== @@ -872,7 +895,6 @@   - [#3090](https://github.com/agda/agda/issues/3090): Internal error in parser when using parentheses in BUILTIN pragma   - [#3096](https://github.com/agda/agda/issues/3096): Support GHC 8.4.3 - Release notes for Agda version 2.5.3 ==================================== @@ -1695,7 +1717,6 @@   - [#2734](https://github.com/agda/agda/issues/2734): Make height of empty lines configurable   - [#2736](https://github.com/agda/agda/issues/2736): Segfault using Alex 3.2.2 and cpphs   - [#2740](https://github.com/agda/agda/issues/2740): Indenting every line of code should be a no-op-  Release notes for Agda version 2.5.2 ====================================

binary file changed (645013 → 640670 bytes)

@@ -1,2 +1,2 @@-(define-package "agda2-mode" "2.5.4.1"+(define-package "agda2-mode" "2.5.4.2"   "interactive development for Agda, a dependently typed functional programming language")

@@ -10,7 +10,7 @@  ;;; Code: -(defvar agda2-version "2.5.4.1"+(defvar agda2-version "2.5.4.2"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.") 

@@ -37,7 +37,7 @@ import Agda.Interaction.Options import Agda.Interaction.FindFile import Agda.Interaction.Highlighting.HTML-import Agda.Interaction.Imports (getAllWarnings')+import Agda.Interaction.Imports (getAllWarnings) import Agda.TypeChecking.Warnings  import Agda.Utils.FileName@@ -165,7 +165,7 @@     Just i  -> sequence_ [ compilerMain backend isMain i | Backend backend <- backends ]    -- print warnings that might have accumulated during compilation-  ws <- filter (not . isUnsolvedWarning . tcWarning) <$> getAllWarnings' AllWarnings RespectFlags+  ws <- filter (not . isUnsolvedWarning . tcWarning) <$> getAllWarnings AllWarnings   unless (null ws) $ reportSDoc "warning" 1 $ P.vcat $ P.prettyTCM <$> ws  

@@ -147,9 +147,9 @@ addImportedThings isig ibuiltin patsyns display userwarn warnings = do   stImports              %= \ imp -> unionSignatures [imp, isig]   stImportedBuiltins     %= \ imp -> Map.union imp ibuiltin+  stImportedUserWarnings %= \ imp -> Map.union imp userwarn   stPatternSynImports    %= \ imp -> Map.union imp patsyns   stImportedDisplayForms %= \ imp -> HMap.unionWith (++) imp display-  stUserWarnings         %= \ imp -> Map.union imp userwarn   stTCWarnings           %= \ imp -> List.union imp warnings   addImportedInstances isig @@ -175,9 +175,9 @@   deriving (Functor, Foldable, Traversable) type MaybeWarnings = MaybeWarnings' [TCWarning] -applyFlagsToMaybeWarnings :: IgnoreFlags -> MaybeWarnings -> TCM MaybeWarnings-applyFlagsToMaybeWarnings r mw = do-  w' <- traverse (applyFlagsToTCWarnings r) mw+applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings+applyFlagsToMaybeWarnings mw = do+  w' <- traverse applyFlagsToTCWarnings mw   return $ if null w' then NoWarnings else w'  instance Null a => Null (MaybeWarnings' a) where@@ -477,7 +477,7 @@                    _                        -> "Checking"       withMsgs = bracket_        (chaseMsg checkMsg x $ Just $ filePath file)-       (const $ do ws <- getAllWarnings' AllWarnings RespectFlags+       (const $ do ws <- getAllWarnings AllWarnings                    let (we, wa) = classifyWarnings ws                    let wa' = filter ((Strict.Just file ==) . tcWarningOrigin) wa                    unless (null wa') $@@ -503,7 +503,7 @@       isig     <- use stImports       ibuiltin <- use stImportedBuiltins       display  <- use stImportsDisplayForms-      userwarn <- use stUserWarnings+      userwarn <- use stImportedUserWarnings       ipatsyns <- getPatternSynImports       ho       <- getInteractionOutputCallback       -- Every interface is treated in isolation. Note: Some changes to@@ -752,7 +752,7 @@       stTokens .= mempty        -- Grabbing warnings and unsolved metas to highlight them-      warnings <- getAllWarnings' AllWarnings RespectFlags+      warnings <- getAllWarnings AllWarnings       unless (null warnings) $ reportSDoc "import.iface.create" 20 $         P.text "collected warnings: " P.<> prettyTCM warnings       unsolved <- getAllUnsolved@@ -812,10 +812,7 @@       ]     reportSLn "import.iface.create" 7 $ "Finished serialization." -    mallWarnings <- getAllWarnings ErrorWarnings-                      $ case isMain of-                          MainInterface _  -> IgnoreFlags-                          NotMainInterface -> RespectFlags+    mallWarnings <- getMaybeWarnings' isMain ErrorWarnings      reportSLn "import.iface.create" 7 $ "Considering writing to interface file."     case (mallWarnings, isMain) of@@ -844,11 +841,6 @@      return $ first constructIScope (i, mallWarnings) --- | Collect all warnings that have accumulated in the state.--- Depending on the argument, we either respect the flags passed--- in by the user, or not (for instance when deciding if we are--- writing an interface file or not)- getUniqueMetasRanges :: [MetaId] -> TCM [Range] getUniqueMetasRanges = fmap List.nub . mapM getMetaRange @@ -871,8 +863,18 @@                 , checkNonEmpty UnsolvedMetaVariables    unsolvedMetas                 , checkNonEmpty UnsolvedConstraints      unsolvedConstraints ] -getAllWarnings' :: WhichWarnings -> IgnoreFlags -> TCM [TCWarning]-getAllWarnings' ww ifs = do++-- | Collect all warnings that have accumulated in the state.++getAllWarnings :: WhichWarnings -> TCM [TCWarning]+getAllWarnings = getAllWarnings' NotMainInterface++-- | Expert version of 'getAllWarnings'; if 'isMain' is a+-- 'MainInterface', the warnings definitely include also unsolved+-- warnings.++getAllWarnings' :: MainInterface -> WhichWarnings -> TCM [TCWarning]+getAllWarnings' isMain ww = do   unsolved            <- getAllUnsolved   collectedTCWarnings <- use stTCWarnings @@ -880,12 +882,15 @@                     not (null unsolved && onlyShowIfUnsolved w)    fmap (filter (showWarn . tcWarning))-    $ applyFlagsToTCWarnings ifs $ reverse+    $ applyFlagsToTCWarnings' isMain $ reverse     $ unsolved ++ collectedTCWarnings -getAllWarnings :: WhichWarnings -> IgnoreFlags -> TCM MaybeWarnings-getAllWarnings ww ifs = do-  allWarnings <- getAllWarnings' ww ifs+getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings+getMaybeWarnings = getMaybeWarnings' NotMainInterface++getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings+getMaybeWarnings' isMain ww = do+  allWarnings <- getAllWarnings' isMain ww   return $ if null allWarnings     -- Andreas, issue 964: not checking null interactionPoints     -- anymore; we want to serialize with open interaction points now!@@ -898,7 +903,7 @@     NonFatalErrors{} -> return []     _ -> localState $ do       put tcst-      ws <- getAllWarnings' ErrorWarnings RespectFlags+      ws <- getAllWarnings AllWarnings       -- We filter out the unsolved(Metas/Constraints) to stay       -- true to the previous error messages.       return $ filter (not . isUnsolvedWarning . tcWarning) ws@@ -946,7 +951,7 @@     display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms     -- TODO: Kill some ranges?     (display, sig) <- eliminateDeadCode display =<< getSignature-    userwarns <- use stUserWarnings+    userwarns <- use stLocalUserWarnings     syntaxInfo <- use stSyntaxInfo     -- Andreas, 2015-02-09 kill ranges in pattern synonyms before     -- serialization to avoid error locations pointing to external files@@ -954,7 +959,7 @@     patsyns <- killRange <$> getPatternSyns     h       <- liftIO $ hashFile file     let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin-    warnings <- getAllWarnings' AllWarnings RespectFlags+    warnings <- getAllWarnings AllWarnings     reportSLn "import.iface" 7 "  instantiating all meta variables"     i <- instantiateFull $ Interface       { iSourceHash      = h

@@ -6,4 +6,10 @@ import Agda.TypeChecking.Monad.Base ( TCM ) import Data.Map                     ( Map ) +data Mode++data MainInterface = MainInterface Mode | NotMainInterface++instance Eq MainInterface+ scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)

@@ -755,7 +755,7 @@             (if b == QuickLaTeX              then Imp.ScopeCheck              else Imp.TypeCheck) $ \(i, mw) -> do-    mw <- lift $ Imp.applyFlagsToMaybeWarnings RespectFlags mw+    mw <- lift $ Imp.applyFlagsToMaybeWarnings mw     case mw of       Imp.NoWarnings -> do         lift $ case b of@@ -1054,7 +1054,7 @@ -- | Show warnings interpretWarnings :: CommandM (String, String) interpretWarnings = do-  mws <- lift $ Imp.getAllWarnings AllWarnings RespectFlags+  mws <- lift $ Imp.getMaybeWarnings AllWarnings   case filter isNotMeta <$> mws of     Imp.SomeWarnings ws@(_:_) -> do       let (we, wa) = classifyWarnings ws

@@ -2,7 +2,6 @@  module Agda.Interaction.Options     ( CommandLineOptions(..)-    , IgnoreFlags(..)     , PragmaOptions(..)     , OptionsPragma     , Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)@@ -60,8 +59,10 @@   )  import Agda.Utils.FileName      ( absolute, AbsolutePath, filePath )-import Agda.Utils.Monad         ( ifM, readM )+import Agda.Utils.Functor       ( (<&>) )+import Agda.Utils.Lens          ( Lens', over ) import Agda.Utils.List          ( groupOn, wordsBy )+import Agda.Utils.Monad         ( ifM, readM ) import Agda.Utils.String        ( indent ) import Agda.Utils.Trie          ( Trie ) import Agda.Syntax.Parser.Literate ( literateExts )@@ -81,11 +82,6 @@  type Verbosity = Trie String Int --- ignore or respect the flags --allow-unsolved-metas,--- --no-termination-check, --no-positivity-check?-data IgnoreFlags = IgnoreFlags | RespectFlags-  deriving Eq- -- Don't forget to update --   doc/user-manual/tools/command-line-options.rst -- if you make changes to the command-line options!@@ -375,7 +371,11 @@ ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True }  allowUnsolvedFlag :: Flag PragmaOptions-allowUnsolvedFlag o = return $ o { optAllowUnsolved = True }+allowUnsolvedFlag o = do+  let upd = over warningSet (Set.\\ unsolvedWarnings)+  return $ o { optAllowUnsolved = True+             , optWarningMode   = upd (optWarningMode o)+             }  showImplicitFlag :: Flag PragmaOptions showImplicitFlag o = return $ o { optShowImplicit = True }@@ -419,10 +419,18 @@ latexDirFlag d o = return $ o { optLaTeXDir = d }  noPositivityFlag :: Flag PragmaOptions-noPositivityFlag o = return $ o { optDisablePositivity = True }+noPositivityFlag o = do+  let upd = over warningSet (Set.delete NotStrictlyPositive_)+  return $ o { optDisablePositivity = True+             , optWarningMode   = upd (optWarningMode o)+             }  dontTerminationCheckFlag :: Flag PragmaOptions-dontTerminationCheckFlag o = return $ o { optTerminationCheck = False }+dontTerminationCheckFlag o = do+  let upd = over warningSet (Set.delete TerminationIssue_)+  return $ o { optTerminationCheck = False+             , optWarningMode   = upd (optWarningMode o)+             }  -- The option was removed. See Issue 1918. dontCompletenessCheckFlag :: Flag PragmaOptions@@ -430,8 +438,8 @@   throwError "the --no-coverage-check option has been removed"  dontUniverseCheckFlag :: Flag PragmaOptions-dontUniverseCheckFlag o = return $ o { optUniverseCheck        = False-                                     }+dontUniverseCheckFlag o = return $ o { optUniverseCheck = False }+ etaFlag :: Flag PragmaOptions etaFlag o = return $ o { optEta = True } @@ -475,10 +483,18 @@ noPatternMatchingFlag o = return $ o { optPatternMatching = False }  exactSplitFlag :: Flag PragmaOptions-exactSplitFlag o = return $ o { optExactSplit = True }+exactSplitFlag o = do+  let upd = over warningSet (Set.insert CoverageNoExactSplit_)+  return $ o { optExactSplit = True+             , optWarningMode   = upd (optWarningMode o)+             }  noExactSplitFlag :: Flag PragmaOptions-noExactSplitFlag o = return $ o { optExactSplit = False }+noExactSplitFlag o = do+  let upd = over warningSet (Set.delete CoverageNoExactSplit_)+  return $ o { optExactSplit = False+             , optWarningMode   = upd (optWarningMode o)+             }  rewritingFlag :: Flag PragmaOptions rewritingFlag o = return $ o { optRewriting = True }@@ -497,10 +513,11 @@   return $ o { optInversionMaxDepth = d }  interactiveFlag :: Flag CommandLineOptions-interactiveFlag  o = return $ o { optInteractive    = True-                                , optPragmaOptions  = (optPragmaOptions o)-                                                      { optAllowUnsolved = True }-                                }+interactiveFlag  o = do+  prag <- allowUnsolvedFlag (optPragmaOptions o)+  return $ o { optInteractive    = True+             , optPragmaOptions = prag+             }  compileFlagNoMain :: Flag PragmaOptions compileFlagNoMain o = return $ o { optCompileNoMain = True }

@@ -6,6 +6,11 @@        , warningSet        , warn2Error        , defaultWarningSet+       , allWarnings+       , usualWarnings+       , noWarnings+       , unsolvedWarnings+       , errorWarnings        , defaultWarningMode        , warningModeUpdate        , warningSets@@ -75,18 +80,46 @@ warningSets :: [(String, (Set WarningName, String))] warningSets = [ ("all"   , (allWarnings, "All of the existing warnings"))               , ("warn"  , (usualWarnings, "Default warning level"))-              , ("ignore", (noWarnings, "Ignore all warnings"))+              , ("ignore", (errorWarnings, "Ignore all the benign warnings"))               ]  noWarnings :: Set WarningName noWarnings = Set.empty +unsolvedWarnings :: Set WarningName+unsolvedWarnings = Set.fromList+                 [ UnsolvedMetaVariables_+                 , UnsolvedInteractionMetas_+                 , UnsolvedConstraints_+                 ]++errorWarnings :: Set WarningName+errorWarnings = Set.fromList+  [ CoverageIssue_+  , GenericNonFatalError_+  , NotStrictlyPositive_+  , OverlappingTokensWarning_+  , SafeFlagPostulate_+  , SafeFlagPragma_+  , SafeFlagNonTerminating_+  , SafeFlagTerminating_+  , SafeFlagPrimTrustMe_+  , SafeFlagNoPositivityCheck_+  , SafeFlagPolarity_+  , TerminationIssue_+  , UnsolvedMetaVariables_+  , UnsolvedInteractionMetas_+  , UnsolvedConstraints_+  ]+ allWarnings :: Set WarningName allWarnings = Set.fromList [minBound..maxBound]  usualWarnings :: Set WarningName usualWarnings = allWarnings Set.\\ Set.fromList-              [ UnknownFixityInMixfixDecl_ ]+              [ UnknownFixityInMixfixDecl_+              , CoverageNoExactSplit_+              ]  -- | The @WarningName@ data enumeration is meant to have a one-to-one correspondance -- to existing warnings in the codebase.

@@ -143,7 +143,7 @@             (Imp.ScopeCheck, _)  -> return Nothing             (_, NoWarnings)      -> return $ Just i             (_, SomeWarnings ws) -> do-              ws' <- applyFlagsToTCWarnings RespectFlags ws+              ws' <- applyFlagsToTCWarnings ws               case ws' of                 []   -> return Nothing                 cuws -> tcWarningsToError cuws@@ -160,7 +160,7 @@             LaTeX.generateLaTeX i            -- Print accumulated warnings-          ws <- (snd . classifyWarnings) <$> Imp.getAllWarnings' AllWarnings RespectFlags+          ws <- (snd . classifyWarnings) <$> Imp.getAllWarnings AllWarnings           unless (null ws) $ do             let banner = text $ "\n" ++ delimiter "All done; warnings encountered"             reportSDoc "warning" 1 $

@@ -514,7 +514,7 @@         -- In case we find a defined name, we start by checking whether there's         -- a warning attached to it         reportSDoc "scope.warning" 50 $ text $ "Checking usage of " ++ prettyShow d-        mstr <- Map.lookup (anameName d) <$> use stUserWarnings+        mstr <- Map.lookup (anameName d) <$> getUserWarnings         forM_ mstr (warning . UserWarning)         -- and then we return the name         return $ nameExpr d@@ -1911,7 +1911,7 @@    toAbstract (C.WarningOnUsage _ oqn str) = do     qn <- toAbstract $ OldName oqn-    stUserWarnings %= Map.insert qn str+    stLocalUserWarnings %= Map.insert qn str     pure []    -- Termination checking pragmes are handled by the nicifier

@@ -10,6 +10,7 @@   , prettyTCWarnings'   , prettyTCWarnings   , tcWarningsToError+  , applyFlagsToTCWarnings'   , applyFlagsToTCWarnings   , dropTopLevelModule   , stringTCErr@@ -33,7 +34,9 @@ import qualified Data.Map as Map import qualified Text.PrettyPrint.Boxes as Boxes +import {-# SOURCE #-} Agda.Interaction.Imports (MainInterface(..)) import Agda.Interaction.Options+import Agda.Interaction.Options.Warnings import Agda.Syntax.Common import Agda.Syntax.Fixity import Agda.Syntax.Notation@@ -60,11 +63,13 @@ import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope ( ifPiType ) import Agda.TypeChecking.Reduce (instantiate)+import Agda.TypeChecking.Warnings  import Agda.Utils.Except ( MonadError(catchError, throwError) ) import Agda.Utils.FileName import Agda.Utils.Function import Agda.Utils.Functor+import Agda.Utils.Lens import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Monad@@ -236,8 +241,8 @@ -- | Depending which flags are set, one may happily ignore some -- warnings. -applyFlagsToTCWarnings :: IgnoreFlags -> [TCWarning] -> TCM [TCWarning]-applyFlagsToTCWarnings ifs ws = do+applyFlagsToTCWarnings' :: MainInterface -> [TCWarning] -> TCM [TCWarning]+applyFlagsToTCWarnings' isMain ws = do    -- For some reason some SafeFlagPragma seem to be created multiple times.   -- This is a way to collect all of them and remove duplicates.@@ -247,45 +252,28 @@                  [TCWarning r (SafeFlagPragma sfp) p b]               _                        -> [] --  unsolvedNotOK <- not . optAllowUnsolved <$> pragmaOptions-  negativeNotOK <- not . optDisablePositivity <$> pragmaOptions-  loopingNotOK  <- optTerminationCheck <$> pragmaOptions-  catchallNotOK <- optExactSplit <$> pragmaOptions+  warnSet <- do+    opts <- pragmaOptions+    let warnSet = optWarningMode opts ^. warningSet+    pure $ if isMain /= NotMainInterface+           then Set.union warnSet unsolvedWarnings+           else warnSet    -- filter out the warnings the flags told us to ignore-  let cleanUp w =-        let ignore = ifs == IgnoreFlags-            keepUnsolved us = not (null us) && (ignore || unsolvedNotOK)-        in case w of-          TerminationIssue{}           -> ignore || loopingNotOK-          CoverageIssue{}              -> ignore || unsolvedNotOK-          NotStrictlyPositive{}        -> ignore || negativeNotOK-          UnsolvedMetaVariables ums    -> keepUnsolved ums-          UnsolvedInteractionMetas uis -> keepUnsolved uis-          UnsolvedConstraints ucs      -> keepUnsolved ucs-          OldBuiltin{}                 -> True-          EmptyRewritePragma           -> True-          UselessPublic                -> True-          ParseWarning{}               -> True-          UnreachableClauses{}         -> True-          InversionDepthReached{}      -> True-          CoverageNoExactSplit{}       -> catchallNotOK-          UselessInline{}              -> True-          GenericWarning{}             -> True-          GenericNonFatalError{}       -> True-          SafeFlagPostulate{}          -> True-          SafeFlagPragma{}             -> False -- dealt with separately-          SafeFlagNonTerminating       -> True-          SafeFlagTerminating          -> True-          SafeFlagPrimTrustMe          -> True-          SafeFlagNoPositivityCheck    -> True-          SafeFlagPolarity             -> True-          DeprecationWarning{}         -> True-          NicifierIssue{}              -> True-          UserWarning{}                -> True +  let cleanUp w = let wName = warningName w in+        wName /= SafeFlagPragma_+        && wName `elem` warnSet+        && case w of+          UnsolvedMetaVariables ums    -> not $ null ums+          UnsolvedInteractionMetas uis -> not $ null uis+          UnsolvedConstraints ucs      -> not $ null ucs+          _                            -> True+   return $ sfp ++ filter (cleanUp . tcWarning) ws++applyFlagsToTCWarnings :: [TCWarning] -> TCM [TCWarning]+applyFlagsToTCWarnings = applyFlagsToTCWarnings' NotMainInterface  --------------------------------------------------------------------------- -- * Helpers

@@ -0,0 +1,117 @@+-- | Free variable check that reduces the subject to make certain variables not+--   free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.+module Agda.TypeChecking.Free.Reduce (forceNotFree) where++import Control.Monad.State+import qualified Data.IntSet as IntSet+import Data.IntSet (IntSet)+import Data.Traversable (traverse)++import Agda.Syntax.Common+import Agda.Syntax.Internal+import Agda.TypeChecking.Monad+import Agda.TypeChecking.Reduce+import Agda.TypeChecking.Substitute+import Agda.TypeChecking.Free.Precompute+import Agda.Utils.Monad++-- | Try to enforce a set of variables not occurring in a given type. Returns a+--   possibly reduced version of the type and the subset of variables that does+--   indeed not occur in the reduced type.+forceNotFree :: IntSet -> Type -> TCM (IntSet, Type)+forceNotFree xs a = do+  (a, xs) <- runStateT (forceNotFreeR $ precomputeFreeVars_ a) xs+  return (xs, a)++class (PrecomputeFreeVars a, Subst Term a) => ForceNotFree a where+  -- Reduce the argument if necessary, to make as many as possible of the+  -- variables in the state not free. Updates the state, removing the variables+  -- that couldn't be make not free. By updating the state as soon as a+  -- variable can not be reduced away, we avoid trying to get rid of it in+  -- other places.+  forceNotFree' :: a -> StateT IntSet TCM a++-- Reduce the argument if there are offending free variables. Doesn't call the+-- continuation when no reduction is required.+reduceIfFreeVars :: (Reduce a, ForceNotFree a) => (a -> StateT IntSet TCM a) -> a -> StateT IntSet TCM a+reduceIfFreeVars k a = do+  xs <- get+  let fvs     = precomputedFreeVars a+      notfree = IntSet.null $ IntSet.intersection xs fvs+  if | notfree   -> return a+     | otherwise -> k . precomputeFreeVars_ =<< lift (reduce a)++-- Careful not to define forceNotFree' = forceNotFreeR since that would loop.+forceNotFreeR :: (Reduce a, ForceNotFree a) => a -> StateT IntSet TCM a+forceNotFreeR = reduceIfFreeVars forceNotFree'++instance (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) where+  -- Precomputed free variables are stored in the Arg so reduceIf outside the+  -- traverse.+  forceNotFree' = reduceIfFreeVars (traverse forceNotFree')++instance (Reduce a, ForceNotFree a) => ForceNotFree (Dom a) where+  forceNotFree' = traverse forceNotFreeR++instance (Reduce a, ForceNotFree a) => ForceNotFree (Abs a) where+  -- Reduction stops at abstractions (lambda/pi) so do reduceIf/forceNotFreeR here.+  forceNotFree' a@NoAbs{} = traverse forceNotFreeR a+  forceNotFree' a@Abs{} =+    -- Shift variables up when going under the abstraction and back down when+    -- coming out of it. Since we only ever remove variables from the state+    -- there's no danger of getting negative indices.+    reduceIfFreeVars (bracket_ (modify $ IntSet.map succ) (\ _ -> modify $ IntSet.map pred) .+                      traverse forceNotFree') a++instance ForceNotFree a => ForceNotFree [a] where+  forceNotFree' = traverse forceNotFree'++instance (Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) where+  -- There's an Arg inside Elim' which stores precomputed free vars, so let's+  -- not skip over that.+  forceNotFree' (Apply arg)    = Apply <$> forceNotFree' arg+  forceNotFree' e@Proj{}       = return e++instance ForceNotFree Type where+  forceNotFree' (El s t) = El <$> forceNotFree' s <*> forceNotFree' t++instance ForceNotFree Term where+  forceNotFree' t = case t of+    Var x es   -> Var x    <$ modify (IntSet.delete x) <*> forceNotFree' es+    Def f es   -> Def f    <$> forceNotFree' es+    Con c h es -> Con c h  <$> forceNotFree' es+    MetaV x es -> MetaV x  <$> forceNotFree' es+    Lam h b    -> Lam h    <$> forceNotFree' b+    Pi a b     -> Pi       <$> forceNotFree' a <*> forceNotFree' b  -- Dom and Abs do reduceIf so not needed here+    Sort s     -> Sort     <$> forceNotFree' s+    Level l    -> Level    <$> forceNotFree' l+    DontCare t -> DontCare <$> forceNotFreeR t  -- Reduction stops at DontCare so reduceIf+    Lit{}      -> return t++instance ForceNotFree Level where+  forceNotFree' (Max as) = Max <$> forceNotFree' as++instance ForceNotFree PlusLevel where+  forceNotFree' l = case l of+    ClosedLevel{} -> return l+    Plus k a      -> Plus k <$> forceNotFree' a++instance ForceNotFree LevelAtom where+  forceNotFree' l = case l of+    MetaLevel x es   -> MetaLevel x    <$> forceNotFree' es+    BlockedLevel x t -> BlockedLevel x <$> forceNotFree' t+    NeutralLevel b t -> NeutralLevel b <$> forceNotFree' t+    UnreducedLevel t -> UnreducedLevel <$> forceNotFreeR t  -- Already reduce in the cases above++instance ForceNotFree Sort where+  -- Reduce for sorts already goes under all sort constructors, so we can get+  -- away without forceNotFreeR here.+  forceNotFree' s = case s of+    Type l     -> Type     <$> forceNotFree' l+    Prop       -> return Prop+    PiSort a b -> PiSort   <$> forceNotFree' a <*> forceNotFree' b+    UnivSort s -> UnivSort <$> forceNotFree' s+    MetaS x es -> MetaS x  <$> forceNotFree' es+    Inf        -> return s+    SizeUniv   -> return s+

@@ -23,6 +23,8 @@ import Data.Monoid import Data.Set (Set) import qualified Data.Set as Set+import qualified Data.IntSet as IntSet+import Data.IntSet (IntSet) import Data.Traversable (traverse)  import qualified Agda.Benchmarking as Bench@@ -35,11 +37,11 @@ import Agda.TypeChecking.Reduce import Agda.TypeChecking.Pretty import Agda.TypeChecking.Free hiding (Occurrence(..))+import Agda.TypeChecking.Free.Reduce import Agda.TypeChecking.Substitute import Agda.TypeChecking.Datatypes import Agda.TypeChecking.Records import {-# SOURCE #-} Agda.TypeChecking.MetaVars--- import Agda.TypeChecking.MetaVars  import Agda.Utils.Either @@ -716,7 +718,7 @@       let a = jMetaType $ mvJudgement mv       TelV tel b <- telView' <$> instantiateFull a       let args         = zip (telToList tel) (kills ++ repeat False)-          (kills', a') = killedType args b+      (kills', a') <- killedType args b       dbg kills' a a'       -- If there is any prunable argument, perform the pruning       if not (any unArg kills') then return PrunedNothing else do@@ -748,14 +750,79 @@ --   Invariant: @k'i == True@ iff @ki == True@ and pruning the @i@th argument from --   type @b@ is possible without creating unbound variables. --   @t'@ is type @t@ after pruning all @k'i==True@.-killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> ([Arg Bool], Type)-killedType [] b = ([], b)-killedType ((arg@(Dom info _), kill) : kills) b-  | dontKill  = (Arg info False : args, mkPi arg b')-  | otherwise = (Arg info True  : args, strengthen __IMPOSSIBLE__ b')+killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> TCM ([Arg Bool], Type)+killedType args b = do++  -- Turn list of bools into an IntSet containing the variables we want to kill+  -- (indices relative to b).+  let tokill = IntSet.fromList [ i | ((_, True), i) <- zip (reverse args) [0..] ]++  -- First, check the free variables of b to see if they prevent any kills.+  (tokill, b) <- reallyNotFreeIn tokill b++  -- Then recurse over the telescope (right-to-left), building up the final type.+  (killed, b) <- go (reverse $ map fst args) tokill b++  -- Turn the IntSet of killed variables into the list of Arg Bool's to return.+  let kills = [ Arg (getArgInfo dom) (IntSet.member i killed)+              | (i, (dom, _)) <- reverse $ zip [0..] $ reverse args ]+  return (kills, b)   where-    (args, b') = killedType kills b-    dontKill = not kill || 0 `freeIn` b'+    down = IntSet.map pred+    up   = IntSet.map succ++    -- go Δ xs B+    -- Invariants:+    --   - Δ ⊢ B+    --   - Δ is represented as a list in right-to-left order+    --   - xs are deBruijn indices into Δ+    --   - xs ∩ FV(B) = Ø+    -- Result: (ys, Δ' → B')+    --    where Δ' ⊆ Δ  (possibly reduced to remove dependencies, see #3177)+    --          ys ⊆ xs are the variables that were dropped from Δ+    --          B' = strengthen ys B+    go :: [Dom (ArgName, Type)] -> IntSet -> Type -> TCM (IntSet, Type)+    go [] xs b | IntSet.null xs = return (xs, b)+               | otherwise      = __IMPOSSIBLE__+    go (arg : args) xs b  -- go (Δ (x : A)) xs B, (x = deBruijn index 0)+      | IntSet.member 0 xs = do+          -- Case x ∈ xs. We know x ∉ FV(B), so we can safely drop x from the+          -- telescope. Drop x from xs (and shift indices) and recurse with+          -- `strengthen x B`.+          let ys = down (IntSet.delete 0 xs)+          (ys, b) <- go args ys $ strengthen __IMPOSSIBLE__ b+          -- We need to return a set of killed variables relative to Δ (x : A), so+          -- shift ys and add x back in.+          return (IntSet.insert 0 $ up ys, b)+      | otherwise = do+          -- Case x ∉ xs. We either can't or don't want to get rid of x. In+          -- this case we have to check A for potential dependencies preventing+          -- us from killing variables in xs.+          let xs'       = down xs -- Shift to make relative to Δ ⊢ A+              (name, a) = unDom arg+          (ys, a) <- reallyNotFreeIn xs' a+          -- Recurse on Δ, ys, and (x : A') → B, where A reduces to A' and ys ⊆ xs'+          -- not free in A'. We already know ys not free in B.+          (zs, b) <- go args ys (mkPi ((name, a) <$ arg) b)+          -- Shift back up to make it relative to Δ (x : A) again.+          return (up zs, b)++reallyNotFreeIn :: IntSet -> Type -> TCM (IntSet, Type)+reallyNotFreeIn xs a | IntSet.null xs = return (xs, a)  -- Shortcut+reallyNotFreeIn xs a = do+  let fvs      = freeVars a+      anywhere = allVars fvs+      rigid    = IntSet.unions [stronglyRigidVars fvs, unguardedVars fvs]+      nonrigid = IntSet.difference anywhere rigid+      hasNo    = IntSet.null . IntSet.intersection xs+  if | hasNo nonrigid ->+        -- No non-rigid occurrences. We can't do anything about the rigid+        -- occurrences so drop those and leave `a` untouched.+        return (IntSet.difference xs rigid, a)+     | otherwise -> do+        -- If there are non-rigid occurrences we need to reduce a to see if+        -- we can get rid of them (#3177).+        forceNotFree (IntSet.difference xs rigid) a  -- | Instantiate a meta variable with a new one that only takes --   the arguments which are not pruneable.

@@ -143,7 +143,10 @@     -- ^ @{-# FOREIGN #-}@ code that should be included in the compiled output.     -- Does not include code for imported modules.   , stPreFreshInteractionId :: !InteractionId-  , stPreUserWarnings       :: !(Map A.QName String)+  , stPreImportedUserWarnings :: !(Map A.QName String)+    -- ^ Imported @UserWarning@s, not to be stored in the @Interface@+  , stPreLocalUserWarnings    :: !(Map A.QName String)+    -- ^ Locally defined @UserWarning@s, to be stored in the @Interface@   }  type DisambiguatedNames = IntMap A.QName@@ -287,7 +290,8 @@   , stPreImportedInstanceDefs = Map.empty   , stPreForeignCode          = Map.empty   , stPreFreshInteractionId   = 0-  , stPreUserWarnings         = Map.empty+  , stPreImportedUserWarnings = Map.empty+  , stPreLocalUserWarnings    = Map.empty   }  initPostScopeState :: PostScopeState@@ -388,10 +392,21 @@   f (stPreFreshInteractionId (stPreScopeState s)) <&>   \x -> s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}} -stUserWarnings :: Lens' (Map A.QName String) TCState-stUserWarnings f s =-  f (stPreUserWarnings (stPreScopeState s)) <&>-  \ x -> s {stPreScopeState = (stPreScopeState s) {stPreUserWarnings = x}}+stImportedUserWarnings :: Lens' (Map A.QName String) TCState+stImportedUserWarnings f s =+  f (stPreImportedUserWarnings (stPreScopeState s)) <&>+  \ x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedUserWarnings = x}}++stLocalUserWarnings :: Lens' (Map A.QName String) TCState+stLocalUserWarnings f s =+  f (stPreLocalUserWarnings (stPreScopeState s)) <&>+  \ x -> s {stPreScopeState = (stPreScopeState s) {stPreLocalUserWarnings = x}}++getUserWarnings :: MonadState TCState m => m (Map A.QName String)+getUserWarnings = do+  iuw <- use stImportedUserWarnings+  luw <- use stLocalUserWarnings+  return $ iuw `Map.union` luw  stBackends :: Lens' [Backend] TCState stBackends f s =

@@ -60,7 +60,7 @@ -- 32-bit machines). Word64 does not have these problems.  currentInterfaceVersion :: Word64-currentInterfaceVersion = 20180518 * 10 + 0+currentInterfaceVersion = 20181021 * 10 + 0  -- | Encodes something. To ensure relocatability file paths in -- positions are replaced with module names.

@@ -35,7 +35,6 @@   icod_ (TerminationIssue a)         = __IMPOSSIBLE__   icod_ (UnreachableClauses a b)     = icodeN 0 UnreachableClauses a b   icod_ (CoverageIssue a b)          = __IMPOSSIBLE__-  icod_ (CoverageNoExactSplit a b)   = __IMPOSSIBLE__   icod_ (NotStrictlyPositive a b)    = __IMPOSSIBLE__   icod_ (UnsolvedMetaVariables a)    = __IMPOSSIBLE__   icod_ (UnsolvedInteractionMetas a) = __IMPOSSIBLE__@@ -58,6 +57,7 @@   icod_ (NicifierIssue a)            = icodeN 7 NicifierIssue a   icod_ (InversionDepthReached a)    = icodeN 8 InversionDepthReached a   icod_ (UserWarning a)              = icodeN 9 UserWarning a+  icod_ (CoverageNoExactSplit a b)   = icodeN 10 CoverageNoExactSplit a b    value = vcase valu where       valu [0, a, b]    = valuN UnreachableClauses a b@@ -70,6 +70,7 @@       valu [7, a]       = valuN NicifierIssue a       valu [8, a]       = valuN InversionDepthReached a       valu [9, a]       = valuN UserWarning a+      valu [10, a, b]   = valuN CoverageNoExactSplit a b       valu _ = malformed  instance EmbPrj DeclarationWarning where

@@ -5,7 +5,7 @@ import qualified Data.Set as Set import qualified Data.List as List import Data.Maybe ( catMaybes )-import Control.Monad (guard, forM_)+import Control.Monad ( guard, forM, unless )  import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Monad.Caching@@ -62,12 +62,18 @@         | onlyOnce w && elem tcwarn tcwarns = tcwarns -- Eq on TCWarning only checks head constructor         | otherwise                         = tcwarn : tcwarns -  forM_ (catMaybes $ applyWarningMode wmode <$> ws) $ \ w' -> do+  -- We collect *all* of the warnings no matter whether they are in the @warningSet@+  -- or not. If we find one which should be turned into an error, we keep processing+  -- the rest of the warnings and *then* report all of the errors at once.+  merrs <- forM ws $ \ w' -> do     tcwarn <- warning_ w'-    if wmode ^. warn2Error-    then typeError $ NonFatalErrors [tcwarn]-    else stTCWarnings %= add w' tcwarn+    if wmode ^. warn2Error && warningName w' `elem` wmode ^. warningSet+    then pure (Just tcwarn)+    else Nothing <$ (stTCWarnings %= add w' tcwarn) +  let errs = catMaybes merrs+  unless (null errs) $ typeError $ NonFatalErrors errs+ {-# SPECIALIZE warning :: Warning -> TCM () #-} warning :: MonadTCM tcm => Warning -> tcm () warning = warnings . pure@@ -82,41 +88,13 @@   deriving (Eq, Ord)  isUnsolvedWarning :: Warning -> Bool-isUnsolvedWarning w = case w of-  UnsolvedMetaVariables{}    -> True-  UnsolvedInteractionMetas{} -> True-  UnsolvedConstraints{}      -> True- -- rest-  _                          -> False+isUnsolvedWarning w = warningName w `elem` unsolvedWarnings  classifyWarning :: Warning -> WhichWarnings-classifyWarning w = case w of-  OldBuiltin{}               -> AllWarnings-  EmptyRewritePragma         -> AllWarnings-  UselessPublic              -> AllWarnings-  UnreachableClauses{}       -> AllWarnings-  UselessInline{}            -> AllWarnings-  GenericWarning{}           -> AllWarnings-  DeprecationWarning{}       -> AllWarnings-  NicifierIssue{}            -> AllWarnings-  InversionDepthReached{}    -> AllWarnings-  UserWarning{}              -> AllWarnings-  TerminationIssue{}         -> ErrorWarnings-  CoverageIssue{}            -> ErrorWarnings-  CoverageNoExactSplit{}     -> ErrorWarnings-  NotStrictlyPositive{}      -> ErrorWarnings-  UnsolvedMetaVariables{}    -> ErrorWarnings-  UnsolvedInteractionMetas{} -> ErrorWarnings-  UnsolvedConstraints{}      -> ErrorWarnings-  GenericNonFatalError{}     -> ErrorWarnings-  SafeFlagPostulate{}        -> ErrorWarnings-  SafeFlagPragma{}           -> ErrorWarnings-  SafeFlagNonTerminating     -> ErrorWarnings-  SafeFlagTerminating        -> ErrorWarnings-  SafeFlagPrimTrustMe        -> ErrorWarnings-  SafeFlagNoPositivityCheck  -> ErrorWarnings-  SafeFlagPolarity           -> ErrorWarnings-  ParseWarning{}             -> ErrorWarnings+classifyWarning w =+  if warningName w `elem` errorWarnings+  then ErrorWarnings+  else AllWarnings  -- | Should we only emit a single warning with this constructor. onlyOnce :: Warning -> Bool

@@ -1,3 +1,6 @@+# The version installed of `cpphs` should match the lower version+# required in Agda.cabal [Issue #2315].+ resolver: lts-6.35  extra-deps:@@ -6,6 +9,7 @@ - equivalence-0.3.2 - async-2.2.1 - gitrev-1.3.1+- text-1.2.3.1  # Local packages, usually specified by relative directory name packages:

@@ -2,6 +2,7 @@  extra-deps: - async-2.2.1+- text-1.2.3.1  # Local packages, usually specified by relative directory name packages:

@@ -1,7 +1,8 @@-resolver: lts-11.11+resolver: lts-11.22  extra-deps: - async-2.2.1+- text-1.2.3.1  # Local packages, usually specified by relative directory name packages:

@@ -1,5 +0,0 @@-resolver: lts-12.0--# Local packages, usually specified by relative directory name-packages:-- '.'

@@ -0,0 +1,5 @@+resolver: lts-12.16++# Local packages, usually specified by relative directory name+packages:+- '.'