summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Errors.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Errors.hs')
-rw-r--r--src/full/Agda/TypeChecking/Errors.hs505
1 files changed, 265 insertions, 240 deletions
diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs
index 66db96d..6dab9be 100644
--- a/src/full/Agda/TypeChecking/Errors.hs
+++ b/src/full/Agda/TypeChecking/Errors.hs
@@ -5,10 +5,15 @@
module Agda.TypeChecking.Errors
( prettyError
+ , prettyWarning
, tcErrString
+ , prettyTCWarnings'
, prettyTCWarnings
, tcWarningsToError
, applyFlagsToTCWarnings
+ , dropTopLevelModule
+ , stringTCErr
+ , sayWhen
) where
import Prelude hiding (null)
@@ -16,6 +21,10 @@ import Prelude hiding (null)
import Control.Monad.Reader
import Control.Monad.State
+#if __GLASGOW_HASKELL__ <= 708
+import Data.Foldable (foldMap)
+#endif
+
import Data.Function
import Data.List (nub, sortBy, intersperse, isInfixOf)
import Data.Maybe
@@ -42,23 +51,27 @@ import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Context
+import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Telescope ( ifPiType )
import Agda.TypeChecking.Reduce (instantiate)
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.Function
+import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
-import Agda.Utils.Size
+import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
+import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
@@ -86,14 +99,14 @@ prettyError err = liftTCM $ show <$> prettyError' err []
---------------------------------------------------------------------------
instance PrettyTCM TCWarning where
- prettyTCM (TCWarning tcst clw) = localState $ do
- put tcst
- sayWhen (envRange $ clEnv clw)
- (envCall $ clEnv clw)
- (prettyTCM $ clValue clw)
+ prettyTCM = return . tcWarningPrintedWarning
instance PrettyTCM Warning where
- prettyTCM wng = case wng of
+ prettyTCM = prettyWarning
+
+{-# SPECIALIZE prettyWarning :: Warning -> TCM Doc #-}
+prettyWarning :: MonadTCM tcm => Warning -> tcm Doc
+prettyWarning wng = liftTCM $ case wng of
UnsolvedMetaVariables ms ->
fsep ( pwords "Unsolved metas at the following locations:" )
@@ -115,19 +128,38 @@ instance PrettyTCM Warning where
then d
else d $$ nest 4 (text "[ at" <+> prettyTCM r <+> text "]")
- TerminationIssue tes ->
+ TerminationIssue tes -> do
+ dropTopLevel <- topLevelModuleDropper
fwords "Termination checking failed for the following functions:"
- $$ (nest 2 $ fsep $ punctuate comma $
- map (pretty . dropTopLevelModule) $
- concatMap termErrFunctions tes)
- $$ fwords "Problematic calls:"
- $$ (nest 2 $ fmap (P.vcat . nub) $
- mapM prettyTCM $ sortBy (compare `on` callInfoRange) $
- concatMap termErrCalls tes)
+ $$ (nest 2 $ fsep $ punctuate comma $
+ map (pretty . dropTopLevel) $
+ concatMap termErrFunctions tes)
+ $$ fwords "Problematic calls:"
+ $$ (nest 2 $ fmap (P.vcat . nub) $
+ mapM prettyTCM $ sortBy (compare `on` callInfoRange) $
+ concatMap termErrCalls tes)
+
+ UnreachableClauses f pss -> fsep $
+ pwords "Unreachable" ++ pwords (plural (length pss) "clause")
+ where
+ plural 1 thing = thing
+ plural n thing = thing ++ "s"
+
+ CoverageIssue f pss -> fsep (
+ pwords "Incomplete pattern matching for" ++ [prettyTCM f <> text "."] ++
+ pwords "Missing cases:") $$ nest 2 (vcat $ map display pss)
+ where
+ display (tel, ps) = prettyTCM $ NamedClause f True $
+ empty { clauseTel = tel, namedClausePats = ps }
+
+ CoverageNoExactSplit f cs -> vcat $
+ [ fsep $ pwords "Exact splitting is enabled, but the following" ++ pwords (singPlural cs "clause" "clauses") ++
+ pwords "could not be preserved as definitional equalities in the translation to a case tree:"
+ ] ++
+ map (nest 2 . prettyTCM . NamedClause f True) cs
NotStrictlyPositive d ocs -> fsep $
- [prettyTCM (dropTopLevelModule d)] ++
- pwords "is not strictly positive, because it occurs"
+ [prettyTCM d] ++ pwords "is not strictly positive, because it occurs"
++ [prettyTCM ocs]
OldBuiltin old new -> fwords $
@@ -136,10 +168,51 @@ instance PrettyTCM Warning where
EmptyRewritePragma -> fsep . pwords $ "Empty REWRITE pragma"
+ UselessPublic -> fwords $ "Keyword `public' is ignored here"
+
+ UselessInline q -> fsep $
+ pwords "It is pointless for INLINE'd function" ++ [prettyTCM q] ++
+ pwords "to have a separate Haskell definition"
+
+ GenericWarning d -> return d
+
+ GenericNonFatalError d -> return d
+
+ SafeFlagPostulate e -> fsep $
+ pwords "Cannot postulate" ++ [pretty e] ++ pwords "with safe flag"
+
+ SafeFlagPragma xs ->
+ let plural | length xs == 1 = ""
+ | otherwise = "s"
+ in fsep $ [fwords ("Cannot set OPTION pragma" ++ plural)]
+ ++ map text xs ++ [fwords "with safe flag."]
+
+ SafeFlagNonTerminating -> fsep $
+ pwords "Cannot use NON_TERMINATING pragma with safe flag."
+
+ SafeFlagTerminating -> fsep $
+ pwords "Cannot use TERMINATING pragma with safe flag."
+
+ SafeFlagPrimTrustMe -> fsep (pwords "Cannot use primTrustMe with safe flag")
+
+ SafeFlagNoPositivityCheck -> fsep $
+ pwords "Cannot use NO_POSITIVITY_CHECK pragma with safe flag."
+
+ SafeFlagPolarity -> fsep $
+ pwords "The POLARITY pragma must not be used in safe mode."
+
ParseWarning pw -> pretty pw
+ DeprecationWarning old new version -> fsep $
+ [text old] ++ pwords "has been deprecated. Use" ++ [text new] ++ pwords
+ "instead. This will be an error in Agda" ++ [text version <> text "."]
+
+ NicifierIssue ws -> vcat $ do
+ for ws $ \ w -> do
+ sayWhere (getRange w) $ pretty w
+
prettyTCWarnings :: [TCWarning] -> TCM String
-prettyTCWarnings = fmap (unlines . intersperse " ") . prettyTCWarnings'
+prettyTCWarnings = fmap (unlines . intersperse "") . prettyTCWarnings'
prettyTCWarnings' :: [TCWarning] -> TCM [String]
prettyTCWarnings' = mapM (fmap show . prettyTCM)
@@ -157,24 +230,51 @@ tcWarningsToError ws = typeError $ case ws of
applyFlagsToTCWarnings :: IgnoreFlags -> [TCWarning] -> TCM [TCWarning]
applyFlagsToTCWarnings ifs 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.
+ let pragmas w = case tcWarning w of { SafeFlagPragma ps -> ([w], ps); _ -> ([], []) }
+ let sfp = case fmap nub (foldMap pragmas ws) of
+ (TCWarning r w p:_, sfp) ->
+ [TCWarning r (SafeFlagPragma sfp) p]
+ _ -> []
+
+
unsolvedNotOK <- not . optAllowUnsolved <$> pragmaOptions
negativeNotOK <- not . optDisablePositivity <$> pragmaOptions
loopingNotOK <- optTerminationCheck <$> pragmaOptions
+ catchallNotOK <- optExactSplit <$> pragmaOptions
+ -- 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
-
- return $ filter (cleanUp . tcWarning) ws
+ UnreachableClauses{} -> 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
+
+ return $ sfp ++ filter (cleanUp . tcWarning) ws
---------------------------------------------------------------------------
-- * Helpers
@@ -199,10 +299,13 @@ nameWithBinding q =
tcErrString :: TCErr -> String
tcErrString err = show (getRange err) ++ " " ++ case err of
- TypeError _ cl -> errorString $ clValue cl
- Exception r s -> show r ++ " " ++ show s
- IOException r e -> show r ++ " " ++ show e
- PatternErr{} -> "PatternErr"
+ TypeError _ cl -> errorString $ clValue cl
+ Exception r s -> show r ++ " " ++ show s
+ IOException _ r e -> show r ++ " " ++ show e
+ PatternErr{} -> "PatternErr"
+
+stringTCErr :: String -> TCErr
+stringTCErr = Exception noRange . P.text
errorString :: TypeError -> String
errorString err = case err of
@@ -224,11 +327,6 @@ errorString err = case err of
ClashingModuleImport{} -> "ClashingModuleImport"
CompilationError{} -> "CompilationError"
ConstructorPatternInWrongDatatype{} -> "ConstructorPatternInWrongDatatype"
- CoverageFailure{} -> "CoverageFailure"
- CoverageCantSplitOn{} -> "CoverageCantSplitOn"
- CoverageCantSplitIrrelevantType{} -> "CoverageCantSplitIrrelevantType"
- CoverageCantSplitType{} -> "CoverageCantSplitType"
- CoverageNoExactSplit{} -> "CoverageNoExactSplit"
CyclicModuleDependency{} -> "CyclicModuleDependency"
DataMustEndInSort{} -> "DataMustEndInSort"
-- UNUSED: DataTooManyParameters{} -> "DataTooManyParameters"
@@ -248,10 +346,7 @@ errorString err = case err of
IllformedProjectionPattern{} -> "IllformedProjectionPattern"
CannotEliminateWithPattern{} -> "CannotEliminateWithPattern"
IllegalLetInTelescope{} -> "IllegalLetInTelescope"
- IncompletePatternMatching{} -> "IncompletePatternMatching"
- IndexVariablesNotDistinct{} -> "IndexVariablesNotDistinct"
- IndicesFreeInParameters{} -> "IndicesFreeInParameters"
- IndicesNotConstructorApplications{} -> "IndicesNotConstructorApplications"
+-- UNUSED: IncompletePatternMatching{} -> "IncompletePatternMatching"
InternalError{} -> "InternalError"
InvalidPattern{} -> "InvalidPattern"
LocalVsImportedModuleClash{} -> "LocalVsImportedModuleClash"
@@ -269,7 +364,6 @@ errorString err = case err of
NoParseForLHS{} -> "NoParseForLHS"
-- NoParseForPatternSynonym{} -> "NoParseForPatternSynonym"
NoRHSRequiresAbsurdPattern{} -> "NoRHSRequiresAbsurdPattern"
- NotInductive {} -> "NotInductive"
AbsurdPatternRequiresNoRHS{} -> "AbsurdPatternRequiresNoRHS"
NoSuchBuiltinName{} -> "NoSuchBuiltinName"
NoSuchModule{} -> "NoSuchModule"
@@ -285,23 +379,16 @@ errorString err = case err of
NotAnExpression{} -> "NotAnExpression"
NotImplemented{} -> "NotImplemented"
NotSupported{} -> "NotSupported"
+ AbstractConstructorNotInScope{} -> "AbstractConstructorNotInScope"
NotInScope{} -> "NotInScope"
NotLeqSort{} -> "NotLeqSort"
NothingAppliedToHiddenArg{} -> "NothingAppliedToHiddenArg"
NothingAppliedToInstanceArg{} -> "NothingAppliedToInstanceArg"
OverlappingProjects {} -> "OverlappingProjects"
- OperatorChangeMessage {} -> "OperatorChangeMessage"
OperatorInformation {} -> "OperatorInformation"
PatternShadowsConstructor {} -> "PatternShadowsConstructor"
PropMustBeSingleton -> "PropMustBeSingleton"
RepeatedVariablesInPattern{} -> "RepeatedVariablesInPattern"
- SafeFlagPostulate{} -> "SafeFlagPostulate"
- SafeFlagPragma{} -> "SafeFlagPragma"
- SafeFlagNonTerminating{} -> "SafeFlagNonTerminating"
- SafeFlagTerminating{} -> "SafeFlagTerminating"
- SafeFlagPrimTrustMe{} -> "SafeFlagPrimTrustMe"
- SafeFlagNoPositivityCheck{} -> "SafeFlagNoPositivityCheck"
- SafeFlagPolarity{} -> "SafeFlagPolarity"
ShadowedModule{} -> "ShadowedModule"
ShouldBeASort{} -> "ShouldBeASort"
ShouldBeApplicationOf{} -> "ShouldBeApplicationOf"
@@ -313,6 +400,7 @@ errorString err = case err of
NotAProjectionPattern{} -> "NotAProjectionPattern"
ShouldEndInApplicationOfTheDatatype{} -> "ShouldEndInApplicationOfTheDatatype"
SplitError{} -> "SplitError"
+ ImpossibleConstructor{} -> "ImpossibleConstructor"
TerminationCheckFailed{} -> "TerminationCheckFailed"
TooFewFields{} -> "TooFewFields"
TooManyArgumentsInLHS{} -> "TooManyArgumentsInLHS"
@@ -328,24 +416,16 @@ errorString err = case err of
UnequalSorts{} -> "UnequalSorts"
UnequalTerms{} -> "UnequalTerms"
UnequalTypes{} -> "UnequalTypes"
- UnifyConflict{} -> "UnifyConflict"
- UnifyCycle{} -> "UnifyCycle"
- UnifyIndicesNotVars{} -> "UnifyIndicesNotVars"
- UnificationRecursiveEq{} -> "UnificationRecursiveEq"
- UnificationStuck{} -> "UnificationStuck"
-- UnequalTelescopes{} -> "UnequalTelescopes" -- UNUSED
- HeterogeneousEquality{} -> "HeterogeneousEquality"
WithOnFreeVariable{} -> "WithOnFreeVariable"
UnexpectedWithPatterns{} -> "UnexpectedWithPatterns"
UninstantiatedDotPattern{} -> "UninstantiatedDotPattern"
UninstantiatedModule{} -> "UninstantiatedModule"
- UnreachableClauses{} -> "UnreachableClauses"
SolvedButOpenHoles{} -> "SolvedButOpenHoles"
UnusedVariableInPatternSynonym -> "UnusedVariableInPatternSynonym"
UnquoteFailed{} -> "UnquoteFailed"
DeBruijnIndexOutOfScope{} -> "DeBruijnIndexOutOfScope"
WithClausePatternMismatch{} -> "WithClausePatternMismatch"
- WithoutKError{} -> "WithoutKError"
WrongHidingInApplication{} -> "WrongHidingInApplication"
WrongHidingInLHS{} -> "WrongHidingInLHS"
WrongHidingInLambda{} -> "WrongHidingInLambda"
@@ -370,9 +450,9 @@ instance PrettyTCM TCErr where
TypeError s e -> localState $ do
put s
sayWhen (envRange $ clEnv e) (envCall $ clEnv e) $ prettyTCM e
- Exception r s -> sayWhere r $ return s
- IOException r e -> sayWhere r $ fwords $ show e
- PatternErr{} -> sayWhere err $ panic "uncaught pattern violation"
+ Exception r s -> sayWhere r $ return s
+ IOException _ r e -> sayWhere r $ fwords $ show e
+ PatternErr{} -> sayWhere err $ panic "uncaught pattern violation"
instance PrettyTCM CallInfo where
prettyTCM c = do
@@ -382,12 +462,20 @@ instance PrettyTCM CallInfo where
then call
else call $$ nest 2 (text "(at" <+> prettyTCM r <> text ")")
--- | Drops the filename component of the qualified name.
+-- | Drops given amount of leading components of the qualified name.
dropTopLevelModule' :: Int -> QName -> QName
dropTopLevelModule' k (QName (MName ns) n) = QName (MName (drop k ns)) n
-dropTopLevelModule :: QName -> QName
-dropTopLevelModule = dropTopLevelModule' 1
+-- | Drops the filename component of the qualified name.
+dropTopLevelModule :: QName -> TCM QName
+dropTopLevelModule q = ($ q) <$> topLevelModuleDropper
+
+-- | Produces a function which drops the filename component of the qualified name.
+topLevelModuleDropper :: TCM (QName -> QName)
+topLevelModuleDropper = do
+ caseMaybeM (asks envCurrentPath) (return id) $ \ f -> do
+ m <- fromMaybe __IMPOSSIBLE__ <$> lookupModuleFromSource f
+ return $ dropTopLevelModule' $ size m
instance PrettyTCM TypeError where
prettyTCM err = case err of
@@ -404,13 +492,10 @@ instance PrettyTCM TypeError where
GenericDocError d -> return d
TerminationCheckFailed because -> do
- dropTopLevelModule <- do
- caseMaybeM (asks envCurrentPath) (return id) $ \ f -> do
- m <- fromMaybe __IMPOSSIBLE__ <$> lookupModuleFromSource f
- return $ dropTopLevelModule' $ size m
+ dropTopLevel <- topLevelModuleDropper
fwords "Termination checking failed for the following functions:"
$$ (nest 2 $ fsep $ punctuate comma $
- map (pretty . dropTopLevelModule) $
+ map (pretty . dropTopLevel) $
concatMap termErrFunctions because)
$$ fwords "Problematic calls:"
$$ (nest 2 $ fmap (P.vcat . nub) $
@@ -457,8 +542,8 @@ instance PrettyTCM TypeError where
WrongHidingInLambda t ->
fwords "Found an implicit lambda where an explicit lambda was expected"
- WrongIrrelevanceInLambda t ->
- fwords "Found an irrelevant lambda where a relevant lambda was expected"
+ WrongIrrelevanceInLambda ->
+ fwords "Found a non-strict lambda where a irrelevant lambda was expected"
WrongNamedArgument a -> fsep $
pwords "Function does not accept argument "
@@ -477,14 +562,13 @@ instance PrettyTCM TypeError where
"Expected " ++ verbalize (Indefinite r') ++ " argument, but found " ++
verbalize (Indefinite r) ++ " argument"
- NotInductive t -> fsep $
- [prettyTCM t] ++ pwords "is not an inductive data type"
-
UninstantiatedDotPattern e -> fsep $
pwords "Failed to infer the value of dotted pattern"
- IlltypedPattern p a -> fsep $
- pwords "Type mismatch"
+ IlltypedPattern p a -> do
+ let ho _ _ = fsep $ pwords "Cannot pattern match on functions"
+ ifPiType a ho $ {- else -} \ _ -> do
+ fsep $ pwords "Type mismatch"
IllformedProjectionPattern p -> fsep $
pwords "Ill-formed projection pattern " ++ [prettyA p]
@@ -522,51 +606,43 @@ instance PrettyTCM TypeError where
[prettyTCM c] ++ pwords "is not a constructor of the datatype"
++ [prettyTCM d]
- IndicesNotConstructorApplications [i] ->
- fwords "The index"
- $$ nest 2 (prettyTCM i)
- $$ fsep (pwords "is not a constructor (or literal) applied to variables" ++
- pwords "(note that parameters count as constructor arguments)")
-
- IndicesNotConstructorApplications is ->
- fwords "The indices"
- $$ nest 2 (vcat $ map prettyTCM is)
- $$ fsep (pwords "are not constructors (or literals) applied to variables" ++
- pwords "(note that parameters count as constructor arguments)")
-
- IndexVariablesNotDistinct vs is ->
- fwords "The variables"
- $$ nest 2 (vcat $ map (\v -> prettyTCM (I.Var v [])) vs)
- $$ fwords "in the indices"
- $$ nest 2 (vcat $ map prettyTCM is)
- $$ fwords "are not distinct (note that parameters count as constructor arguments)"
-
- IndicesFreeInParameters vs indices pars ->
- fwords "The variables"
- $$ nest 2 (vcat $ map (\v -> prettyTCM (I.Var v [])) vs)
- $$ fwords "which are used (perhaps as constructor parameters) in the index expressions"
- $$ nest 2 (vcat $ map prettyTCM indices)
- $$ fwords "are free in the parameters"
- $$ nest 2 (vcat $ map prettyTCM pars)
-
ShadowedModule x [] -> __IMPOSSIBLE__
- ShadowedModule x ms@(m : _) -> fsep $
- pwords "Duplicate definition of module" ++ [prettyTCM x <> text "."] ++
- pwords "Previous definition of" ++ [help m] ++ pwords "module" ++ [prettyTCM x] ++
- pwords "at" ++ [prettyTCM r]
- where
- help m = do
- b <- isDatatypeModule m
- if b then text "datatype" else empty
+ ShadowedModule x ms@(m0 : _) -> do
+ -- Clash! Concrete module name x already points to the abstract names ms.
+ (r, m) <- do
+ -- Andreas, 2017-07-28, issue #719.
+ -- First, we try to find whether one of the abstract names @ms@ points back to @x@
+ scope <- getScope
+ -- Get all pairs (y,m) such that y points to some m ∈ ms.
+ let xms0 = ms >>= \ m -> map (,m) $ inverseScopeLookupModule m scope
+ reportSLn "scope.clash.error" 30 $ "candidates = " ++ prettyShow xms0
+
+ -- Try to find x (which will have a different Range, if it has one (#2649)).
+ let xms = filter ((\ y -> not (null $ getRange y) && y == C.QName x) . fst) xms0
+ reportSLn "scope.class.error" 30 $ "filtered candidates = " ++ prettyShow xms
+
+ -- If we found a copy of x with non-empty range, great!
+ ifJust (headMaybe xms) (\ (x', m) -> return (getRange x', m)) $ {-else-} do
+
+ -- If that failed, we pick the first m from ms which has a nameBindingSite.
+ let rms = ms >>= \ m -> map (,m) $
+ filter (noRange /=) $ map nameBindingSite $ reverse $ mnameToList m
+ -- Andreas, 2017-07-25, issue #2649
+ -- Take the first nameBindingSite we can get hold of.
+ reportSLn "scope.class.error" 30 $ "rangeful clashing modules = " ++ prettyShow rms
+
+ -- If even this fails, we pick the first m and give no range.
+ return $ fromMaybe (noRange, m0) $ headMaybe rms
- r = case [ r | r <- map (defSiteOfLast . mnameToList) ms
- , r /= noRange ] of
- [] -> noRange
- r : _ -> r
-
- defSiteOfLast [] = noRange
- defSiteOfLast ns = nameBindingSite (last ns)
+ fsep $
+ pwords "Duplicate definition of module" ++ [prettyTCM x <> text "."] ++
+ pwords "Previous definition of" ++ [help m] ++ pwords "module" ++ [prettyTCM x] ++
+ pwords "at" ++ [prettyTCM r]
+ where
+ help m = caseMaybeM (isDatatypeModule m) empty $ \case
+ IsData -> text "(datatype)"
+ IsRecord -> text "(record)"
ModuleArityMismatch m EmptyTel args -> fsep $
pwords "The module" ++ [prettyTCM m] ++
@@ -603,7 +679,8 @@ instance PrettyTCM TypeError where
SplitOnIrrelevant p t -> fsep $
pwords "Cannot pattern match" ++ [prettyA p] ++
- pwords "against irrelevant type" ++ [prettyTCM t]
+ pwords "against" ++ [text $ verbalize $ getRelevance t] ++
+ pwords "argument of type" ++ [prettyTCM t]
DefinitionIsIrrelevant x -> fsep $
text "Identifier" : prettyTCM x : pwords "is declared irrelevant, so it cannot be used here"
@@ -627,11 +704,6 @@ instance PrettyTCM TypeError where
UnequalTypes cmp a b -> prettyUnequal a (notCmp cmp) b
-- fsep $ [prettyTCM a, notCmp cmp, prettyTCM b]
- HeterogeneousEquality u a v b -> fsep $
- pwords "Refuse to solve heterogeneous constraint" ++
- [prettyTCM u] ++ pwords ":" ++ [prettyTCM a] ++ pwords "=?=" ++
- [prettyTCM v] ++ pwords ":" ++ [prettyTCM b]
-
UnequalRelevance cmp a b -> fsep $
[prettyTCM a, notCmp cmp, prettyTCM b] ++
-- Andreas 2010-09-21 to reveal Forced annotations, print also uglily
@@ -681,8 +753,7 @@ instance PrettyTCM TypeError where
WithClausePatternMismatch p q -> fsep $
pwords "With clause pattern " ++ [prettyA p] ++
- pwords " is not an instance of its parent pattern " ++ [prettyTCM q]
- -- TODO: prettier printing for internal patterns
+ pwords " is not an instance of its parent pattern " ++ [P.fsep <$> prettyTCMPatterns [q]]
MetaCannotDependOn m ps i -> fsep $
pwords "The metavariable" ++ [prettyTCM $ MetaV m []] ++
@@ -741,8 +812,9 @@ instance PrettyTCM TypeError where
pwords "The module" ++ [prettyTCM m] ++
pwords "can refer to either a local module or an imported module"
- SolvedButOpenHoles ->
- text "Module cannot be imported since it has open interaction points"
+ SolvedButOpenHoles -> fsep $
+ pwords "Module cannot be imported since it has open interaction points" ++
+ pwords "(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this module)"
CyclicModuleDependency ms ->
fsep (pwords "cyclic module dependency:")
@@ -790,6 +862,11 @@ instance PrettyTCM TypeError where
BothWithAndRHS -> fsep $ pwords "Unexpected right hand side"
+ AbstractConstructorNotInScope q -> fsep $
+ [ text "Constructor"
+ , prettyTCM q
+ ] ++ pwords "is abstract, thus, not in scope here"
+
NotInScope xs -> do
inscope <- Set.toList . concreteNamesInScope <$> getScope
fsep (pwords "Not in scope:") $$ nest 2 (vcat $ map (name inscope) xs)
@@ -834,8 +911,10 @@ instance PrettyTCM TypeError where
where
help :: ModuleName -> TCM Doc
help m = do
- b <- isDatatypeModule m
- sep [prettyTCM m, if b then text "(datatype module)" else empty]
+ anno <- caseMaybeM (isDatatypeModule m) (return empty) $ \case
+ IsData -> return $ text "(datatype module)"
+ IsRecord -> return $ text "(record module)"
+ sep [prettyTCM m, anno ]
UninstantiatedModule x -> fsep (
pwords "Cannot access the contents of the parameterised module"
@@ -1078,15 +1157,6 @@ instance PrettyTCM TypeError where
LeftAssoc -> "infixl"
RightAssoc -> "infixr"
- OperatorChangeMessage err@(OperatorInformation [] _) ->
- prettyTCM err
- OperatorChangeMessage err ->
- prettyTCM err
- $+$
- fsep (pwords $
- "(the treatment of operators was changed in Agda 2.5.1, " ++
- "so code that used to parse may have to be changed)")
-
{- UNUSED
AmbiguousParseForPatternSynonym p ps -> fsep (
pwords "Don't know how to parse" ++ [pretty p <> text "."] ++
@@ -1094,85 +1164,19 @@ instance PrettyTCM TypeError where
) $$ nest 2 (vcat $ map pretty ps)
-}
+{- UNUSED
IncompletePatternMatching v args -> fsep $
pwords "Incomplete pattern matching for" ++ [prettyTCM v <> text "."] ++
pwords "No match for" ++ map prettyTCM args
-
- UnreachableClauses f pss -> fsep $
- pwords "Unreachable" ++ pwords (plural (length pss) "clause")
- where
- plural 1 thing = thing
- plural n thing = thing ++ "s"
-
- CoverageFailure f pss -> fsep (
- pwords "Incomplete pattern matching for" ++ [prettyTCM f <> text "."] ++
- pwords "Missing cases:") $$ nest 2 (vcat $ map display pss)
- where
- display ps = do
- ps <- nicify f ps
- prettyTCM f <+> fsep (map (prettyArg . fmap namedThing) ps)
-
- nicify f ps = do
- showImp <- showImplicitArguments
- if showImp
- then return ps
- else return ps -- TODO: remove implicit arguments which aren't constructors
-
- CoverageCantSplitOn c tel cIxs gIxs
- | length cIxs /= length gIxs -> __IMPOSSIBLE__
- | otherwise -> addContext tel $ vcat (
- [ fsep $ pwords "I'm not sure if there should be a case for the constructor" ++
- [prettyTCM c <> text ","] ++
- pwords "because I get stuck when trying to solve the following" ++
- pwords "unification problems (inferred index ≟ expected index):"
- ] ++
- zipWith (\c g -> nest 2 $ prettyTCM c <+> text "≟" <+> prettyTCM g) cIxs gIxs)
-
- CoverageCantSplitIrrelevantType a -> fsep $
- pwords "Cannot split on argument of irrelevant datatype" ++ [prettyTCM a]
-
-
- CoverageCantSplitType a -> fsep $
- pwords "Cannot split on argument of non-datatype" ++ [prettyTCM a]
-
- CoverageNoExactSplit f cs -> fsep $
- pwords "Exact splitting is enabled, but not all clauses can be preserved as definitional equalities in the translation to a case tree"
+-}
SplitError e -> prettyTCM e
- WithoutKError a u v -> fsep $
- pwords "Cannot eliminate reflexive equation" ++ [prettyTCM u] ++
- pwords "=" ++ [prettyTCM v] ++ pwords "of type" ++ [prettyTCM a] ++
- pwords "because K has been disabled."
-
- UnifyConflict c c' -> fsep $
- pwords "This case is impossible because of a conflict between the constructors " ++
- [prettyTCM c] ++ pwords " and " ++ [prettyTCM c' <> text "."] ++
+ ImpossibleConstructor c neg -> fsep $
+ pwords "The case for the constructor " ++ [prettyTCM c] ++
+ pwords " is impossible" ++ [prettyTCM neg] ++
pwords "Possible solution: remove the clause, or use an absurd pattern ()."
- UnifyCycle i u -> fsep $
- pwords "This case is impossible because the variable " ++ [prettyTCM (var i)] ++
- pwords "occurs strongly rigid in" ++ [prettyTCM u <> text "."] ++
- pwords "Possible solution: remove the clause, or use an absurd pattern ()."
-
- UnifyIndicesNotVars a u v ixs -> fsep $
- pwords "Cannot apply injectivity to the equation" ++ [prettyTCM u] ++
- pwords "=" ++ [prettyTCM v] ++ pwords "of type" ++ [prettyTCM a] ++
- pwords "because I cannot generalize over the indices" ++
- [prettyList $ map prettyTCM ixs]
-
- UnificationRecursiveEq a i u -> fsep $
- pwords "Cannot solve variable " ++ [prettyTCM (var i)] ++
- pwords " of type " ++ [prettyTCM a] ++
- pwords " with solution " ++ [prettyTCM u] ++
- pwords " because the variable occurs in the solution," ++
- pwords " or in the type one of the variables in the solution"
-
- UnificationStuck tel us vs -> fsep $
- pwords "I got stuck on unifying" ++ [prettyList (map prettyTCM us)] ++
- pwords "with" ++ [prettyList (map prettyTCM vs)] ++
- pwords "in the telescope" ++ [prettyTCM tel]
-
TooManyPolarities x n -> fsep $
pwords "Too many polarities given in the POLARITY pragma for" ++
[prettyTCM x] ++
@@ -1210,30 +1214,8 @@ instance PrettyTCM TypeError where
where
cxt' = cxt `abstract` raise (size cxt) (nameCxt names)
nameCxt [] = EmptyTel
- nameCxt (x : xs) = ExtendTel (defaultDom (El I.Prop $ I.Var 0 [])) $ NoAbs (show x) $ nameCxt xs
-
- SafeFlagPostulate e -> fsep $
- pwords "Cannot postulate" ++ [pretty e] ++ pwords "with safe flag"
-
- SafeFlagPragma xs ->
- let plural | length xs == 1 = ""
- | otherwise = "s"
- in fsep $ [fwords ("Cannot set OPTION pragma" ++ plural)]
- ++ map text xs ++ [fwords "with safe flag."]
-
- SafeFlagNonTerminating -> fsep $
- pwords "Cannot use NON_TERMINATING pragma with safe flag."
-
- SafeFlagTerminating -> fsep $
- pwords "Cannot use TERMINATING pragma with safe flag."
-
- SafeFlagPrimTrustMe -> fsep (pwords "Cannot use primTrustMe with safe flag")
-
- SafeFlagNoPositivityCheck -> fsep $
- pwords "Cannot use NO_POSITIVITY_CHECK pragma with safe flag."
-
- SafeFlagPolarity -> fsep $
- pwords "The POLARITY pragma must not be used in safe mode."
+ nameCxt (x : xs) = ExtendTel (defaultDom (El I.Prop $ I.var 0)) $
+ NoAbs (P.prettyShow x) $ nameCxt xs
NeedOptionCopatterns -> fsep $
pwords "Option --copatterns needed to enable destructor patterns"
@@ -1244,7 +1226,7 @@ instance PrettyTCM TypeError where
NonFatalErrors ws -> foldr1 ($$) $ fmap prettyTCM ws
InstanceSearchDepthExhausted c a d -> fsep $
- pwords ("Instance search depth exhaused (max depth: " ++ show d ++ ") for candidate") ++
+ pwords ("Instance search depth exhausted (max depth: " ++ show d ++ ") for candidate") ++
[hang (prettyTCM c <+> text ":") 2 (prettyTCM a)]
where
@@ -1254,13 +1236,14 @@ instance PrettyTCM TypeError where
prettyArg :: Arg (I.Pattern' a) -> TCM Doc
prettyArg (Arg info x) = case getHiding info of
- Hidden -> braces $ prettyPat 0 x
- Instance -> dbraces $ prettyPat 0 x
- NotHidden -> prettyPat 1 x
+ Hidden -> braces $ prettyPat 0 x
+ Instance{} -> dbraces $ prettyPat 0 x
+ NotHidden -> prettyPat 1 x
prettyPat :: Integer -> (I.Pattern' a) -> TCM Doc
prettyPat _ (I.VarP _) = text "_"
prettyPat _ (I.DotP _) = text "._"
+ prettyPat _ (I.AbsurdP _) = text absurdPatternName
prettyPat n (I.ConP c _ args) =
mpar n args $
prettyTCM c <+> fsep (map (prettyArg . fmap namedThing) args)
@@ -1317,11 +1300,10 @@ instance PrettyUnequal Type where
instance PrettyTCM SplitError where
prettyTCM err = case err of
NotADatatype t -> enterClosure t $ \ t -> fsep $
- pwords "Cannot pattern match on non-datatype" ++ [prettyTCM t]
+ pwords "Cannot split on argument of non-datatype" ++ [prettyTCM t]
IrrelevantDatatype t -> enterClosure t $ \ t -> fsep $
- pwords "Cannot pattern match on datatype" ++ [prettyTCM t] ++
- pwords "since it is declared irrelevant"
+ pwords "Cannot split on argument of irrelevant datatype" ++ [prettyTCM t]
CoinductiveDatatype t -> enterClosure t $ \ t -> fsep $
pwords "Cannot pattern match on the coinductive type" ++ [prettyTCM t]
@@ -1332,11 +1314,55 @@ instance PrettyTCM SplitError where
pwords "because it has no constructor"
-}
- CantSplit c tel cIxs gIxs ->
- prettyTCM $ CoverageCantSplitOn c tel cIxs gIxs
+ UnificationStuck c tel cIxs gIxs errs
+ | length cIxs /= length gIxs -> __IMPOSSIBLE__
+ | otherwise -> vcat $
+ [ fsep $ pwords "I'm not sure if there should be a case for the constructor" ++
+ [prettyTCM c <> text ","] ++
+ pwords "because I get stuck when trying to solve the following" ++
+ pwords "unification problems (inferred index ≟ expected index):"
+ ] ++
+ zipWith (\c g -> nest 2 $ addContext tel $ prettyTCM c <+> text "≟" <+> prettyTCM g) cIxs gIxs ++
+ if null errs then [] else
+ [ fsep $ pwords "Possible" ++ pwords (singPlural errs "reason" "reasons") ++
+ pwords "why unification failed:" ] ++
+ map (nest 2 . prettyTCM) errs
GenericSplitError s -> fsep $ pwords "Split failed:" ++ pwords s
+instance PrettyTCM NegativeUnification where
+ prettyTCM err = case err of
+ UnifyConflict tel u v -> addContext tel $ vcat $
+ [ fsep $ pwords "because unification ended with a conflicting equation "
+ , nest 2 $ prettyTCM u <+> text "≟" <+> prettyTCM v
+ ]
+
+ UnifyCycle tel i u -> addContext tel $ vcat $
+ [ fsep $ pwords "because unification ended with a cyclic equation "
+ , nest 2 $ prettyTCM (var i) <+> text "≟" <+> prettyTCM u
+ ]
+
+instance PrettyTCM UnificationFailure where
+ prettyTCM err = case err of
+ UnifyIndicesNotVars tel a u v ixs -> addContext tel $ fsep $
+ pwords "Cannot apply injectivity to the equation" ++ [prettyTCM u] ++
+ pwords "=" ++ [prettyTCM v] ++ pwords "of type" ++ [prettyTCM a] ++
+ pwords "because I cannot generalize over the indices" ++
+ [prettyList (map prettyTCM ixs) <> text "."]
+
+ UnifyRecursiveEq tel a i u -> addContext tel $ fsep $
+ pwords "Cannot solve variable " ++ [prettyTCM (var i)] ++
+ pwords " of type " ++ [prettyTCM a] ++
+ pwords " with solution " ++ [prettyTCM u] ++
+ pwords " because the variable occurs in the solution," ++
+ pwords " or in the type of one of the variables in the solution."
+
+ UnifyReflexiveEq tel a u -> addContext tel $ fsep $
+ pwords "Cannot eliminate reflexive equation" ++ [prettyTCM u] ++
+ pwords "=" ++ [prettyTCM u] ++ pwords "of type" ++ [prettyTCM a] ++
+ pwords "because K has been disabled."
+
+
instance PrettyTCM Call where
prettyTCM c = case c of
CheckClause t cl -> do
@@ -1465,9 +1491,9 @@ class Verbalize a where
instance Verbalize Hiding where
verbalize h =
case h of
- Hidden -> "hidden"
- NotHidden -> "visible"
- Instance -> "instance"
+ Hidden -> "hidden"
+ NotHidden -> "visible"
+ Instance{} -> "instance"
instance Verbalize Relevance where
verbalize r =
@@ -1475,8 +1501,7 @@ instance Verbalize Relevance where
Relevant -> "relevant"
Irrelevant -> "irrelevant"
NonStrict -> "shape-irrelevant"
- Forced{} -> __IMPOSSIBLE__
- UnusedArg -> __IMPOSSIBLE__
+ Forced{} -> "forced"
-- | Indefinite article.
data Indefinite a = Indefinite a