#9672: Error message too long (full case statement printed) -------------------------------------+------------------------------------- Reporter: andreas.abel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: Other Difficulty: Easy (less than 1 | Test Case: hour) | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- 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: }}} {{{#!hs 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") } }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9672 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler