Error message too long (full case statement printed)
Imho, it does not make sense to print the other branches of a case when a type error is discovered in one branch. When you see the following example, you will agree with me.
src/full/Agda/TypeChecking/Errors.hs:540:35:
Couldn't match type ‘[Char]’ with ‘TCMT IO Doc’
Expected type: TCM Doc
Actual type: [Char]
In the expression:
"Module cannot be imported since it has open interaction points"
In a case alternative:
SolvedButOpenHoles
-> "Module cannot be imported since it has open interaction points"
In a stmt of a 'do' block: case err of {
InternalError s -> panic s
NotImplemented s -> fwords $ "Not implemented: " ++ s
NotSupported s -> fwords $ "Not supported: " ++ s
CompilationError s -> sep [fwords "Compilation error:", text s]
GenericError s -> fwords s
GenericDocError d -> return d
TerminationCheckFailed because
-> fwords
"Termination checking failed for the following functions:"
$$
(nest 2
$ fsep
$ punctuate comma
$ map (pretty . dropTopLevelModule)
$ concatMap termErrFunctions because)
$$ fwords "Problematic calls:"
$$
(nest 2
$ fmap (P.vcat . nub)
$ mapM prettyTCM
$ sortBy (compare `on` callInfoRange)
$ concatMap termErrCalls because)
PropMustBeSingleton
-> fwords
"Datatypes in Prop must have at most one constructor when proof irrelevance is enabled"
DataMustEndInSort t
-> fsep
$ pwords "The type of a datatype must end in a sort."
++ [prettyTCM t] ++ pwords "isn't a sort."
ShouldEndInApplicationOfTheDatatype t
-> fsep
$ pwords
"The target of a constructor must be the datatype applied to its parameters,"
++ [prettyTCM t] ++ pwords "isn't"
ShouldBeAppliedToTheDatatypeParameters s t
-> fsep
$ pwords "The target of the constructor should be"
++ [prettyTCM s] ++ pwords "instead of" ++ [prettyTCM t]
ShouldBeApplicationOf t q
-> fsep
$ pwords "The pattern constructs an element of"
++ [prettyTCM q] ++ pwords "which is not the right datatype"
ShouldBeRecordType t
-> fsep
$ pwords "Expected non-abstract record type, found "
++ [prettyTCM t]
ShouldBeRecordPattern p -> fsep $ pwords "Expected record pattern"
NotAProjectionPattern p
-> fsep
$ pwords "Not a valid projection for a copattern: " ++ [prettyA p]
DifferentArities
-> fwords
"The number of arguments in the defining equations differ"
WrongHidingInLHS -> do { fwords "Unexpected implicit argument" }
WrongHidingInLambda t
-> do { fwords
"Found an implicit lambda where an explicit lambda was expected" }
WrongIrrelevanceInLambda t
-> do { fwords
"Found an irrelevant lambda where a relevant lambda was expected" }
WrongNamedArgument a
-> fsep
$ pwords "Function does not accept argument " ++ [prettyTCM a]
WrongHidingInApplication t
-> do { fwords
"Found an implicit application where an explicit application was expected" }
HidingMismatch h h'
-> fwords
$ "Expected "
++
verbalize (Indefinite h')
++
" argument, but found " ++ verbalize (Indefinite h) ++ " argument"
RelevanceMismatch r r'
-> fwords
$ "Expected "
++
verbalize (Indefinite r')
++
" argument, but found " ++ verbalize (Indefinite r) ++ " argument"
ColorMismatch c c'
-> fsep
$ pwords "Expected argument color to be"
++ [prettyTCM c'] ++ pwords "but found color" ++ [prettyTCM c]
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"
IllformedProjectionPattern p
-> fsep $ pwords "Ill-formed projection pattern " ++ [prettyA p]
CannotEliminateWithPattern p a
-> do { let ...;
fsep
$ pwords "Cannot eliminate type"
++
prettyTCM a
: if isProj then
pwords "with projection pattern" ++ ...
else
pwords "with pattern"
++ prettyA p : pwords "(did you supply too many arguments?)" }
TooManyArgumentsInLHS a
-> fsep
$ pwords
"Left hand side gives too many arguments to a function of type"
++ [prettyTCM a]
WrongNumberOfConstructorArguments c expect given
-> fsep
$ pwords "The constructor"
++
[prettyTCM c]
++
pwords "expects"
++
[text (show expect)]
++
pwords "arguments (including hidden ones), but has been given"
++ [text (show given)] ++ pwords "(including hidden ones)"
CantResolveOverloadedConstructorsTargetingSameDatatype d cs
-> fsep
$ pwords
("Can't resolve overloaded constructors targeting the same datatype ("
++ show (qnameToConcrete d) ++ "):")
++ map pretty cs
DoesNotConstructAnElementOf c t
-> fsep
$ pwords "The constructor"
++
[prettyTCM c]
++ pwords "does not construct an element of" ++ [prettyTCM t]
ConstructorPatternInWrongDatatype c d
-> fsep
$ [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 []
-> (throwImpossible
(Impossible "src/full/Agda/TypeChecking/Errors.hs" 404))
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 { ... }
r = case ... of {
[] -> ...
r : _ -> ... }
defSiteOfLast [] = noRange
defSiteOfLast ns = nameBindingSite (last ns)
ModuleArityMismatch m EmptyTel args
-> fsep
$ pwords "The module"
++
[prettyTCM m]
++ pwords "is not parameterized, but is being applied to arguments"
ModuleArityMismatch m tel@(ExtendTel _ _) args
-> fsep
$ pwords "The arguments to "
++
[prettyTCM m]
++ pwords "does not fit the telescope" ++ [prettyTCM tel]
ShouldBeEmpty t []
-> fsep
$ [prettyTCM t]
++ pwords "should be empty, but that's not obvious to me"
ShouldBeEmpty t ps
-> fsep
([prettyTCM t]
++
pwords
"should be empty, but the following constructor patterns are valid:")
$$ nest 2 (vcat $ map (showPat 0) ps)
ShouldBeASort t
-> fsep $ [prettyTCM t] ++ pwords "should be a sort, but it isn't"
ShouldBePi t
-> fsep
$ [prettyTCM t] ++ pwords "should be a function type, but it isn't"
NotAProperTerm -> fwords "Found a malformed term"
SetOmegaNotValidType -> fwords "Set\969 is not a valid type"
InvalidType v
-> fsep $ [prettyTCM v] ++ pwords "is not a valid type"
SplitOnIrrelevant p t
-> fsep
$ pwords "Cannot pattern match"
++ [prettyA p] ++ pwords "against irrelevant type" ++ [prettyTCM t]
DefinitionIsIrrelevant x
-> fsep
$ text "Identifier"
: prettyTCM x
: pwords "is declared irrelevant, so it cannot be used here"
VariableIsIrrelevant x
-> fsep
$ text "Variable"
: prettyTCM x
: pwords "is declared irrelevant, so it cannot be used here"
UnequalBecauseOfUniverseConflict cmp s t
-> fsep $ [prettyTCM s, notCmp cmp, ....]
UnequalTerms cmp s t a
-> do { (d1, d2, d) <- prettyInEqual s t;
fsep $ [...] ++ pwords "of type" ++ [...] ++ [...] }
UnequalTypes cmp a b -> prettyUnequal a (notCmp cmp) b
UnequalColors a b -> error "TODO guilhem 4"
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, ....]
++
pwords
"because one is a relevant function type and the other is an irrelevant function type"
UnequalHiding a b
-> fsep
$ [prettyTCM a, text "!=", ....]
++
pwords
"because one is an implicit function type and the other is an explicit function type"
UnequalSorts s1 s2 -> fsep $ [prettyTCM s1, text "!=", ....]
NotLeqSort s1 s2
-> fsep
$ pwords
"The type of the constructor does not fit in the sort of the datatype, since"
++
[prettyTCM s1]
++ pwords "is not less or equal than" ++ [prettyTCM s2]
TooFewFields r xs
-> fsep
$ pwords "Missing fields"
++
punctuate comma (map pretty xs)
++ pwords "in an element of the record" ++ [prettyTCM r]
TooManyFields r xs
-> fsep
$ pwords "The record type"
++
[prettyTCM r]
++
pwords "does not have the fields"
++ punctuate comma (map pretty xs)
DuplicateConstructors xs
-> fsep
$ pwords "Duplicate constructors"
++ punctuate comma (map pretty xs) ++ pwords "in datatype"
DuplicateFields xs
-> fsep
$ pwords "Duplicate fields"
++ punctuate comma (map pretty xs) ++ pwords "in record"
UnexpectedWithPatterns ps
-> fsep
$ pwords "Unexpected with patterns"
++ (punctuate (text " |") $ map prettyA ps)
WithClausePatternMismatch p q
-> fsep
$ pwords "With clause pattern "
++
[prettyA p]
++
pwords " is not an instance of its parent pattern "
++ [prettyTCM q]
MetaCannotDependOn m ps i
-> fsep
$ pwords "The metavariable"
++
[prettyTCM $ MetaV m []]
++
pwords "cannot depend on"
++ [pvar i] ++ pwords "because it" ++ deps
where
pvar = prettyTCM . var
deps
= case map pvar ps of {
[] -> ...
[x] -> ...
xs -> ... }
MetaOccursInItself m
-> fsep
$ pwords "Cannot construct infinite solution of metavariable"
++ [prettyTCM $ MetaV m []]
BuiltinMustBeConstructor s e
-> fsep
$ [prettyA e]
++
pwords "must be a constructor in the binding to builtin"
++ [text s]
NoSuchBuiltinName s
-> fsep $ pwords "There is no built-in thing called" ++ [text s]
DuplicateBuiltinBinding b x y
-> fsep
$ pwords "Duplicate binding for built-in thing"
++
[text b <> comma] ++ pwords "previous binding to" ++ [prettyTCM x]
NoBindingForBuiltin x
-> fsep
$ pwords "No binding for builtin thing"
++
[text x <> comma]
++
pwords
("use {-# BUILTIN " ++ x ++ " name #-} to bind it to 'name'")
NoSuchPrimitiveFunction x
-> fsep
$ pwords "There is no primitive function called" ++ [text x]
BuiltinInParameterisedModule x
-> fwords
$ "The BUILTIN pragma cannot appear inside a bound context "
++
"(for instance, in a parameterised module or as a local declaration)"
IllegalLetInTelescope tb
-> fsep
$ [pretty tb] ++ pwords " is not allowed in a telescope here."
NoRHSRequiresAbsurdPattern ps
-> fwords
$ "The right-hand side can only be omitted if there "
++ "is an absurd pattern, () or {}, in the left-hand side."
AbsurdPatternRequiresNoRHS ps
-> fwords
$ "The right-hand side must be omitted if there "
++ "is an absurd pattern, () or {}, in the left-hand side."
LocalVsImportedModuleClash m
-> fsep
$ pwords "The module"
++
[text $ show m]
++
pwords "can refer to either a local module or an imported module"
SolvedButOpenHoles
-> "Module cannot be imported since it has open interaction points"
UnsolvedMetas rs
-> fsep (pwords "Unsolved metas at the following locations:")
$$ nest 2 (vcat $ map prettyTCM rs)
UnsolvedConstraints cs
-> fsep (pwords "Failed to solve the following constraints:")
$$ nest 2 (vcat $ map prettyConstraint cs)
where
prettyConstraint :: ProblemConstraint -> TCM Doc
prettyConstraint c
= f (prettyTCM c)
where
r = ...
....
CyclicModuleDependency ms
-> fsep (pwords "cyclic module dependency:")
$$ nest 2 (vcat $ map pretty ms)
FileNotFound x files
-> fsep
(pwords "Failed to find source of module"
++ [pretty x] ++ pwords "in any of the following locations:")
$$ nest 2 (vcat $ map (text . filePath) files)
OverlappingProjects f m1 m2
-> fsep
(pwords "The file"
++
[text (filePath f)]
++
pwords "can be accessed via several project roots. Both"
++
[pretty m1]
++ pwords "and" ++ [pretty m2] ++ pwords "point to this file.")
AmbiguousTopLevelModuleName x files
-> fsep
(pwords "Ambiguous module name. The module name"
++
[pretty x] ++ pwords "could refer to any of the following files:")
$$ nest 2 (vcat $ map (text . filePath) files)
ClashingFileNamesFor x files
-> fsep
(pwords "Multiple possible sources for module"
++ [text $ show x] ++ pwords "found:")
$$ nest 2 (vcat $ map (text . filePath) files)
ModuleDefinedInOtherFile mod file file'
-> fsep
$ pwords "You tried to load"
++
[text (filePath file)]
++
pwords "which defines the module"
++
[pretty mod <> text "."]
++
pwords "However, according to the include path this module should"
++ pwords "be defined in" ++ [text (filePath file') <> text "."]
ModuleNameDoesntMatchFileName given files
-> fsep
(pwords
"The name of the top level module does not match the file name. The module"
++
[pretty given]
++ pwords "should be defined in one of the following files:")
$$ nest 2 (vcat $ map (text . filePath) files)
BothWithAndRHS -> fsep $ pwords "Unexpected right hand side"
NotInScope xs
-> fsep (pwords "Not in scope:") $$ nest 2 (vcat $ map name xs)
where
name x = fsep [...]
suggestion s
| elem ':' s = parens $ text "did you forget space around the ':'?"
| elem "->" two
= parens $ text "did you forget space around the '->'?"
| otherwise = empty
where
two = ...
NoSuchModule x -> fsep $ pwords "No such module" ++ [pretty x]
AmbiguousName x ys
-> vcat
[fsep
$ pwords "Ambiguous name"
++ [...] ++ pwords "It could refer to any one of",
nest 2 $ vcat $ map nameWithBinding ys, ....]
AmbiguousModule x ys
-> vcat
[fsep
$ pwords "Ambiguous module name"
++ [...] ++ pwords "It could refer to any one of",
nest 2 $ vcat $ map help ys, ....]
where
help :: ModuleName -> TCM Doc
help m = do { ... }
UninstantiatedModule x
-> fsep
(pwords "Cannot access the contents of the parameterised module"
++
[pretty x <> text "."]
++
pwords
"To do this the module first has to be instantiated. For instance:")
$$ nest 2 (hsep [text "module", pretty x <> text "'", ....])
ClashingDefinition x y
-> fsep
$ pwords "Multiple definitions of"
++
[pretty x <> text "."]
++
pwords "Previous definition at"
++ [prettyTCM $ nameBindingSite $ qnameName y]
ClashingModule m1 m2
-> fsep
$ pwords "The modules"
++ [prettyTCM m1, text "and", ....] ++ pwords "clash."
ClashingImport x y
-> fsep
$ pwords "Import clash between" ++ [pretty x, text "and", ....]
ClashingModuleImport x y
-> fsep
$ pwords "Module import clash between"
++ [pretty x, text "and", ....]
PatternShadowsConstructor x c
-> fsep
$ pwords "The pattern variable"
++
[prettyTCM x]
++ pwords "has the same name as the constructor" ++ [prettyTCM c]
DuplicateImports m xs
-> fsep
$ pwords "Ambiguous imports from module"
++ [pretty m] ++ pwords "for" ++ punctuate comma (map pretty xs)
ModuleDoesntExport m xs
-> fsep
$ pwords "The module"
++
[pretty m]
++
pwords "doesn't export the following:"
++ punctuate comma (map pretty xs)
NotAModuleExpr e
-> fsep
$ pwords
"The right-hand side of a module definition must have the form 'M e1 .. en'"
++
pwords "where M is a module name. The expression"
++ [pretty e, text "doesn't."]
FieldOutsideRecord
-> fsep $ pwords "Field appearing outside record declaration."
InvalidPattern p
-> fsep $ pretty p : pwords "is not a valid pattern"
RepeatedVariablesInPattern xs
-> fsep
$ pwords "Repeated variables in left hand side:" ++ map pretty xs
NotAnExpression e
-> fsep $ [pretty e] ++ pwords "is not a valid expression."
NotAValidLetBinding nd -> fwords $ "Not a valid let-declaration"
NothingAppliedToHiddenArg e
-> fsep
$ [pretty e]
++
pwords "cannot appear by itself. It needs to be the argument to"
++ pwords "a function expecting an implicit argument."
NothingAppliedToInstanceArg e
-> fsep
$ [pretty e]
++
pwords "cannot appear by itself. It needs to be the argument to"
++ pwords "a function expecting an instance argument."
NoParseForApplication es
-> fsep
$ pwords "Could not parse the application"
++ [pretty $ C.RawApp noRange es]
AmbiguousParseForApplication es es'
-> fsep
(pwords "Don't know how to parse"
++ [pretty_es <> (text ".")] ++ pwords "Could mean any one of:")
$$ nest 2 (vcat $ map pretty' es')
where
pretty_es :: TCM Doc
pretty_es = pretty $ C.RawApp noRange es
pretty' :: C.Expr -> TCM Doc
....
BadArgumentsToPatternSynonym x
-> fsep
$ pwords "Bad arguments to pattern synonym " ++ [prettyTCM x]
TooFewArgumentsToPatternSynonym x
-> fsep
$ pwords "Too few arguments to pattern synonym " ++ [prettyTCM x]
UnusedVariableInPatternSynonym
-> fsep $ pwords "Unused variable in pattern synonym."
NoParseForLHS IsLHS p
-> fsep $ pwords "Could not parse the left-hand side" ++ [pretty p]
NoParseForLHS IsPatSyn p
-> fsep
$ pwords "Could not parse the pattern synonym" ++ [pretty p]
AmbiguousParseForLHS lhsOrPatSyn p ps
-> fsep
(pwords "Don't know how to parse"
++ [pretty_p <> text "."] ++ pwords "Could mean any one of:")
$$ nest 2 (vcat $ map pretty' ps)
where
pretty_p :: TCM Doc
pretty_p = pretty p
pretty' :: C.Pattern -> TCM Doc
....
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 { ... }
nicify f ps = do { ... }
CoverageCantSplitOn c tel cIxs gIxs
| length cIxs /= length gIxs
-> (throwImpossible
(Impossible "src/full/Agda/TypeChecking/Errors.hs" 750))
| otherwise
-> addCtxTel tel
$ vcat
([fsep
$ pwords
"I'm not sure if there should be a case for the constructor"
++
[...]
++
pwords "because I get stuck when trying to solve the following"
++
pwords
"unification problems (inferred index \8799 expected index):"]
++
zipWith
(\ c g -> nest 2 $ prettyTCM c <+> text "\8799" <+> 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]
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."
NotStrictlyPositive d ocs
-> fsep
$ pwords "The datatype"
++
[prettyTCM d]
++ pwords "is not strictly positive, because" ++ prettyOcc "it" ocs
where
prettyOcc _ [] = []
prettyOcc it (OccCon d c r : ocs) = concat [...]
prettyOcc it (OccClause f n r : ocs) = concat [...]
prettyR NonPositively = pwords "negatively"
prettyR (ArgumentTo i q)
= pwords "as the" ++ [...] ++ pwords "argument to" ++ [...]
th 0 = text "first"
th 1 = text "second"
th 2 = text "third"
th n = text (show $ n - 1) <> text "th"
....
IFSNoCandidateInScope t
-> fsep
$ pwords "No variable of type"
++ [prettyTCM t] ++ pwords "was found in scope."
SafeFlagPostulate e
-> fsep
$ pwords "Cannot postulate"
++ [pretty e] ++ pwords "with safe flag"
SafeFlagPragma xs
-> let
plural
| length xs == 1 = ...
| otherwise = ...
in
fsep
$ [fwords ("Cannot set OPTION pragma" ++ plural)]
++ map text xs ++ [fwords "with safe flag."]
SafeFlagNoTerminationCheck
-> fsep
(pwords "Cannot use NO_TERMINATION_CHECK pragma 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")
NeedOptionCopatterns
-> fsep
(pwords
"Option --copatterns needed to enable destructor patterns") }Trac metadata
| Trac field | Value |
|---|---|
| Version | 7.8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |