summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndresSicardRamirez <>2018-10-29 16:58:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-10-29 16:58:00 (GMT)
commit70d2d7d8bf6b49b06d8b140620247eafffbc7dd5 (patch)
treefc7b70a9a790ac49769c15605dbee5ecfa292c9a
parente579926b3d1142f4920960ea34905b3d53af1db5 (diff)
version 2.5.4.22.5.4.2
-rw-r--r--Agda.cabal26
-rw-r--r--CHANGELOG.md25
-rw-r--r--doc/user-manual.pdfbin645013 -> 640670 bytes
-rw-r--r--src/data/emacs-mode/agda2-mode-pkg.el2
-rw-r--r--src/data/emacs-mode/agda2-mode.el2
-rw-r--r--src/full/Agda/Compiler/Backend.hs4
-rw-r--r--src/full/Agda/Interaction/Imports.hs55
-rw-r--r--src/full/Agda/Interaction/Imports.hs-boot6
-rw-r--r--src/full/Agda/Interaction/InteractionTop.hs4
-rw-r--r--src/full/Agda/Interaction/Options.hs53
-rw-r--r--src/full/Agda/Interaction/Options/Warnings.hs37
-rw-r--r--src/full/Agda/Main.hs4
-rw-r--r--src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs4
-rw-r--r--src/full/Agda/TypeChecking/Errors.hs62
-rw-r--r--src/full/Agda/TypeChecking/Free/Reduce.hs117
-rw-r--r--src/full/Agda/TypeChecking/MetaVars/Occurs.hs85
-rw-r--r--src/full/Agda/TypeChecking/Monad/Base.hs27
-rw-r--r--src/full/Agda/TypeChecking/Serialise.hs2
-rw-r--r--src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs3
-rw-r--r--src/full/Agda/TypeChecking/Warnings.hs54
-rw-r--r--stack-7.10.3.yaml4
-rw-r--r--stack-8.0.2.yaml1
-rw-r--r--stack-8.2.2.yaml3
-rw-r--r--stack-8.4.4.yaml (renamed from stack-8.4.3.yaml)2
24 files changed, 424 insertions, 158 deletions
diff --git a/Agda.cabal b/Agda.cabal
index 1869093..7768590 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -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 @@ description:
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 @@ extra-source-files: CHANGELOG.md
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 head
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 @@ flag enable-cluster-counting
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 @@ library
, 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 @@ library
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 @@ library
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
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 40a8e3b..98cb43d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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 @@ For 2.5.4, the following issues have been closed
- [#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
====================================
@@ -1696,7 +1718,6 @@ For 2.5.3, the following issues have been fixed
- [#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
====================================
diff --git a/doc/user-manual.pdf b/doc/user-manual.pdf
index d1962e0..9fbc6d7 100644
--- a/doc/user-manual.pdf
+++ b/doc/user-manual.pdf
Binary files differ
diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el
index 6a13520..753fe4e 100644
--- a/src/data/emacs-mode/agda2-mode-pkg.el
+++ b/src/data/emacs-mode/agda2-mode-pkg.el
@@ -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")
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
index 69aebaf..4cbcd01 100644
--- a/src/data/emacs-mode/agda2-mode.el
+++ b/src/data/emacs-mode/agda2-mode.el
@@ -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.")
diff --git a/src/full/Agda/Compiler/Backend.hs b/src/full/Agda/Compiler/Backend.hs
index c8f2f4f..f7da823 100644
--- a/src/full/Agda/Compiler/Backend.hs
+++ b/src/full/Agda/Compiler/Backend.hs
@@ -37,7 +37,7 @@ import Agda.TypeChecking.Pretty as P
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 @@ backendInteraction backends _ check = do
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
diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index 850315e..656349c 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -147,9 +147,9 @@ addImportedThings ::
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 @@ data MaybeWarnings' a = NoWarnings | SomeWarnings a
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 @@ typeCheck x file isMain = do
_ -> "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 @@ typeCheck x file isMain = do
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 @@ createInterface file mname isMain = Bench.billTo [Bench.TopModule mname] $
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 @@ createInterface file mname isMain = Bench.billTo [Bench.TopModule mname] $
]
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 @@ createInterface file mname isMain = Bench.billTo [Bench.TopModule mname] $
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 @@ getAllUnsolved = do
, 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 @@ getAllWarnings' ww ifs = do
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 @@ errorWarningsOfTCErr err = case err of
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 @@ buildInterface file topLevel pragmas = do
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 @@ buildInterface file topLevel pragmas = do
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
diff --git a/src/full/Agda/Interaction/Imports.hs-boot b/src/full/Agda/Interaction/Imports.hs-boot
index fbe1950..576eb55 100644
--- a/src/full/Agda/Interaction/Imports.hs-boot
+++ b/src/full/Agda/Interaction/Imports.hs-boot
@@ -6,4 +6,10 @@ import Agda.Syntax.Scope.Base ( Scope )
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)
diff --git a/src/full/Agda/Interaction/InteractionTop.hs b/src/full/Agda/Interaction/InteractionTop.hs
index 86f06c4..90c9dfe 100644
--- a/src/full/Agda/Interaction/InteractionTop.hs
+++ b/src/full/Agda/Interaction/InteractionTop.hs
@@ -755,7 +755,7 @@ interpret (Cmd_compile b file argv) =
(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 @@ interpret Cmd_abort = return ()
-- | 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
diff --git a/src/full/Agda/Interaction/Options.hs b/src/full/Agda/Interaction/Options.hs
index 26153ab..5dffa96 100644
--- a/src/full/Agda/Interaction/Options.hs
+++ b/src/full/Agda/Interaction/Options.hs
@@ -2,7 +2,6 @@
module Agda.Interaction.Options
( CommandLineOptions(..)
- , IgnoreFlags(..)
, PragmaOptions(..)
, OptionsPragma
, Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)
@@ -60,8 +59,10 @@ import Agda.Utils.Except
)
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 @@ isLiterate file = any (`isSuffixOf` file) literateExts
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 :: Flag CommandLineOptions
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 :: FilePath -> Flag CommandLineOptions
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 @@ dontCompletenessCheckFlag _ =
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 :: Flag PragmaOptions
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 @@ inversionMaxDepthFlag s o = do
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 }
diff --git a/src/full/Agda/Interaction/Options/Warnings.hs b/src/full/Agda/Interaction/Options/Warnings.hs
index 3a81fbe..bedba95 100644
--- a/src/full/Agda/Interaction/Options/Warnings.hs
+++ b/src/full/Agda/Interaction/Options/Warnings.hs
@@ -6,6 +6,11 @@ module Agda.Interaction.Options.Warnings
, warningSet
, warn2Error
, defaultWarningSet
+ , allWarnings
+ , usualWarnings
+ , noWarnings
+ , unsolvedWarnings
+ , errorWarnings
, defaultWarningMode
, warningModeUpdate
, warningSets
@@ -75,18 +80,46 @@ warningModeUpdate str = case str of
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.
diff --git a/src/full/Agda/Main.hs b/src/full/Agda/Main.hs
index 31f916d..e36510e 100644
--- a/src/full/Agda/Main.hs
+++ b/src/full/Agda/Main.hs
@@ -143,7 +143,7 @@ runAgdaWithOptions backends generateHTML interaction progName opts
(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 @@ runAgdaWithOptions backends generateHTML interaction progName opts
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 $
diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index b829d23..9598ddc 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -514,7 +514,7 @@ instance ToAbstract OldQName A.Expr where
-- 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 @@ instance ToAbstract C.Pragma [A.Pragma] where
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
diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs
index 6f2d214..57d500c 100644
--- a/src/full/Agda/TypeChecking/Errors.hs
+++ b/src/full/Agda/TypeChecking/Errors.hs
@@ -10,6 +10,7 @@ module Agda.TypeChecking.Errors
, prettyTCWarnings'
, prettyTCWarnings
, tcWarningsToError
+ , applyFlagsToTCWarnings'
, applyFlagsToTCWarnings
, dropTopLevelModule
, stringTCErr
@@ -33,7 +34,9 @@ import qualified Data.Set as Set
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.Pretty
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 @@ tcWarningsToError ws = typeError $ case ws of
-- | 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,46 +252,29 @@ applyFlagsToTCWarnings ifs ws = do
[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
---------------------------------------------------------------------------
diff --git a/src/full/Agda/TypeChecking/Free/Reduce.hs b/src/full/Agda/TypeChecking/Free/Reduce.hs
new file mode 100644
index 0000000..f07877d
--- /dev/null
+++ b/src/full/Agda/TypeChecking/Free/Reduce.hs
@@ -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
+
diff --git a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
index 8ad1b71..eddcd77 100644
--- a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
+++ b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
@@ -23,6 +23,8 @@ import Data.Foldable (foldMap)
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 qualified Agda.TypeChecking.Monad.Benchmark as Bench
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 @@ killArgs kills m = do
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 @@ killArgs kills m = do
-- 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.
diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
index f755f82..ac5a844 100644
--- a/src/full/Agda/TypeChecking/Monad/Base.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -143,7 +143,10 @@ data PreScopeState = PreScopeState
-- ^ @{-# 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 @@ initPreScopeState = PreScopeState
, stPreImportedInstanceDefs = Map.empty
, stPreForeignCode = Map.empty
, stPreFreshInteractionId = 0
- , stPreUserWarnings = Map.empty
+ , stPreImportedUserWarnings = Map.empty
+ , stPreLocalUserWarnings = Map.empty
}
initPostScopeState :: PostScopeState
@@ -388,10 +392,21 @@ stFreshInteractionId f s =
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 =
diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs
index 91e48c4..74607e1 100644
--- a/src/full/Agda/TypeChecking/Serialise.hs
+++ b/src/full/Agda/TypeChecking/Serialise.hs
@@ -60,7 +60,7 @@ import Agda.Utils.Except
-- 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.
diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
index 7118fdf..430b04f 100644
--- a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
+++ b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
@@ -35,7 +35,6 @@ instance EmbPrj Warning where
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 @@ instance EmbPrj Warning where
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 @@ instance EmbPrj Warning where
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
diff --git a/src/full/Agda/TypeChecking/Warnings.hs b/src/full/Agda/TypeChecking/Warnings.hs
index 0b0f9df..c4d53d9 100644
--- a/src/full/Agda/TypeChecking/Warnings.hs
+++ b/src/full/Agda/TypeChecking/Warnings.hs
@@ -5,7 +5,7 @@ module Agda.TypeChecking.Warnings where
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,11 +62,17 @@ warnings ws = do
| 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 ()
@@ -82,41 +88,13 @@ data WhichWarnings =
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
diff --git a/stack-7.10.3.yaml b/stack-7.10.3.yaml
index 5b052e5..ea99f74 100644
--- a/stack-7.10.3.yaml
+++ b/stack-7.10.3.yaml
@@ -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 @@ extra-deps:
- 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:
diff --git a/stack-8.0.2.yaml b/stack-8.0.2.yaml
index a36ecff..6c0faad 100644
--- a/stack-8.0.2.yaml
+++ b/stack-8.0.2.yaml
@@ -2,6 +2,7 @@ resolver: lts-9.21
extra-deps:
- async-2.2.1
+- text-1.2.3.1
# Local packages, usually specified by relative directory name
packages:
diff --git a/stack-8.2.2.yaml b/stack-8.2.2.yaml
index ad785c3..3995337 100644
--- a/stack-8.2.2.yaml
+++ b/stack-8.2.2.yaml
@@ -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:
diff --git a/stack-8.4.3.yaml b/stack-8.4.4.yaml
index 126917d..5ce8867 100644
--- a/stack-8.4.3.yaml
+++ b/stack-8.4.4.yaml
@@ -1,4 +1,4 @@
-resolver: lts-12.0
+resolver: lts-12.16
# Local packages, usually specified by relative directory name
packages: