October 2014 - ghc-tickets

[GHC] #8944: Warn instead of stopping on misplaced Haddock comments
by GHC 17 Aug '18

17 Aug '18

#8944: Warn instead of stopping on misplaced Haddock comments -------------------------------------+------------------------------------- Reporter: Fuuzetsu | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Parser) | Version: 7.9 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- Given a simple module like {{{ module H where data F = F () -- ^ Comment for first type argument () }}} and trying to run Haddock on it, we'll get back {{{ /tmp/H.hs:4:12: parse error on input ‘(’ }}} The error message is rather sub-par in this scenario. It'd be great if we could instead print a warning saying that a Haddock comment is unexpected in that position and then continue on parsing. Best case scenario would be a more informative message such as “Documenting each constructor argument is not supported” but that might be quite a bit harder. Filing on GHC Trac as it's the parser that needs changing I believe. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8944> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #9214: UNPACK support for sum types
by GHC 11 Aug '18

11 Aug '18

#9214: UNPACK support for sum types ------------------------------------+------------------------------------- Reporter: mojojojo | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Currently the pragma only supports single-constructor types. So in the following example it will simply be ignored: {{{ data A = A1 Char | A2 {-# UNPACK #-} !B data B = B1 Int | B2 Bool }}} However the problem seems to be easily solvable by denormalizing the type {{{A}}} to something like the following during unpacking: {{{ data A = A1 Char | A2_1 Int | -- from B1 A2_2 Bool -- from B2 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9214> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 9

[GHC] #9334: Implement "instance chains"
by GHC 09 Aug '18

09 Aug '18

#9334: Implement "instance chains" -------------------------------------+------------------------------------- Reporter: diatchki | Owner: diatchki Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.9 checker) | Differential Revisions: Keywords: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------- It would be useful to implement a version of "instance chains" [1] in GHC, which would eliminate the need for OVERLAPPING_INSTANCES in most (all practcial?) programs. The idea is that programmers can explicitly group and order instances into an "instance chain". For example: {{{ instance (Monad m) => StateM (StateT s m) s where ... else (MonadTrans t, StateM m s) => StateM (t m) s where ... }}} When GHC searches for instances, the instances in a chain are considered together and in order, starting with the first one: 1. If the goal matches the current instance's head, then this instance is selected and the rest are ignored, as if they were not there; 2. If the goal does not match the current instance's head, AND it does not unify with the current instance's head, then we skip the instance and proceed to the next member of the chain; 3. If the goal does not match the current instance's head, but it does unify with it, then we cannot use this chain to solve the goal. In summary: earlier instances in a chain "hide" later instances, and later instances can be reached only if we are sure that none of the previous instance will match. [1] http://web.cecs.pdx.edu/~mpj/pubs/instancechains.pdf -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9334> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 19

[GHC] #8128: Standalone deriving fails for GADTs due to inaccessible code
by GHC 24 Jul '18

24 Jul '18

#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.7 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: Unknown/Multiple | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- Consider the following: {{{ {-# LANGUAGE StandaloneDeriving, GADTs, FlexibleInstances #-} module StandaloneDerivingGADT where data T a where MkT1 :: T Int MkT2 :: (Bool -> Bool) -> T Bool deriving instance Show (T Int) }}} This gives the error: {{{ StandaloneDerivingGADT.hs:9:1: Couldn't match type ‛Int’ with ‛Bool’ Inaccessible code in a pattern with constructor MkT2 :: (Bool -> Bool) -> T Bool, in an equation for ‛showsPrec’ In the pattern: MkT2 b1 In an equation for ‛showsPrec’: showsPrec a (MkT2 b1) = showParen ((a >= 11)) ((.) (showString "MkT2 ") (showsPrec 11 b1)) When typechecking the code for ‛showsPrec’ in a standalone derived instance for ‛Show (T Int)’: To see the code I am typechecking, use -ddump-deriv In the instance declaration for ‛Show (T Int)’ }}} The derived instance declaration matches on all the constructors, even if they cannot possibly match. It should omit obviously inaccessible constructors so that this example is accepted. For reference, the derived code is: {{{ instance GHC.Show.Show (StandaloneDerivingGADT.T GHC.Types.Int) where GHC.Show.showsPrec _ StandaloneDerivingGADT.MkT1 = GHC.Show.showString "MkT1" GHC.Show.showsPrec a_aij (StandaloneDerivingGADT.MkT2 b1_aik) = GHC.Show.showParen ((a_aij GHC.Classes.>= 11)) ((GHC.Base..) (GHC.Show.showString "MkT2 ") (GHC.Show.showsPrec 11 b1_aik)) GHC.Show.showList = GHC.Show.showList__ (GHC.Show.showsPrec 0) }}} The same problem applies to other derivable classes (e.g. `Eq`). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8128> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15

[GHC] #8740: Code conditionally compiles
by GHC 24 Jul '18

24 Jul '18

#8740: Code conditionally compiles ----------------------------+---------------------------------------------- Reporter: | Owner: thomaseding | Status: new Type: bug | Milestone: Priority: normal | Version: 7.6.3 Component: Compiler | Operating System: MacOS X Keywords: | Type of failure: GHC rejects valid program Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: Unknown | Blocked By: | Related Tickets: | ----------------------------+---------------------------------------------- {{{ {-# LANGUAGE GADTs #-} {-# LANGUAGE StandaloneDeriving #-} data Abstract data Reified data Player data Elect p a where ElectRefAsTypeOf :: Int -> Elect Abstract a -> Elect Abstract a ElectHandle :: a -> Elect Reified a Controller :: Elect Abstract Player Owner :: Elect Abstract Player You :: Elect Abstract Player deriving instance (Eq a) => Eq (Elect p a) deriving instance (Ord a) => Ord (Elect p a) }}} As is, the above code fails to compile. But if I move `ElectRefAsTypeOf` to be the last constructor for the GADT, the code does compile. If I remove one of the `Elect Abstract Player` constructors, the code still won't compile even if the `ElectRefAsTypeOf` is moved. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8740> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #9599: app runs 10 times faster when compiled with profilling information than without it
by GHC 21 Jul '18

21 Jul '18

#9599: app runs 10 times faster when compiled with profilling information than without it -------------------------------------+------------------------------------- Reporter: kgardas | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Solaris Architecture: x86 | Type of failure: Runtime Difficulty: Unknown | performance bug Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Hello, I've found interesting application code which when compiled with {{{ -O2 -threaded --make }}} runs 10 times slower than the same code compiled with {{{ -O2 -threaded --make -prof -auto-all -caf-all -fforce-recomp }}} the application is compiled by GHC 7.8.2 on i386-solaris2 platform. The profiling application is then run as normal application, i.e. without +RTS -p. The application itself is my crude beginner Haskell code which takes Wikipedia dump (XML file) and tries wiki pages from there import into XWiki using REST API. It uses Data.Text package for lazy load of Wikipedia data, whole logic of selection of page/title/content is done on Data.Text and later saved into XPage which is using ByteString. The application also uses Simon Marlow's Async/async/wait code which is copied from Simon Marlow's Parallel and Concurrent Programming in Haskell http://chimera.labs.oreilly.com/books/1230000000929 App attached. My question is, what to do with it to help finding the issue? E.g. I assume it's issue when profiling app is that much faster than common optimized app. For your information, optimized app takes 9m50s to upload 1000 pages while profiled optimized app takes only 50s to upload the same amount of pages on my equipped with E5-2620 (2 GHz 6 core/12 threads xeon) Also the difference in time is that big that it's not caused by a noise in import of pages on XWiki side. I've tested several times of course. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9599> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #8581: Add support for explicitly-bidirectional pattern synonyms
by GHC 12 Jul '18

12 Jul '18

#8581: Add support for explicitly-bidirectional pattern synonyms ------------------------------------+------------------------------------- Reporter: cactus | Owner: cactus Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: 5144 | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Some patterns cannot, by themselves, be turned over into an expression, so they have to be defined as unidirectional. Maybe the most trivial example would be {{{ pattern P -> _ }}} Sometimes, however, it would be desirable to give an explicit way of turning these pattern synonyms into expressions. The PatternSynonyms wiki page has this example: {{{ import qualified Data.Sequence as Seq pattern Empty -> (Seq.viewl -> Seq.EmptyL) pattern x :< xs -> (Seq.viewl -> x Seq.:< xs) pattern xs :> x -> (Seq.viewr -> xs Seq.:> x) }}} It would make a ton of sense to be able to use this cons/snoc notation as "constructors" for `Seq`s. The proposed syntax for this {{{ pattern x :< xs -> (Seq.viewl -> x Seq.:< xs) where x :< xs = x Seq.<| xs }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8581> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 52

[GHC] #8822: Allow -- ^ Haddock syntax on record constructors
by GHC 10 Jul '18

10 Jul '18

#8822: Allow -- ^ Haddock syntax on record constructors -------------------------------------+------------------------------------- Reporter: Fuuzetsu | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Parser) | Version: 7.9 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- Original ticket is on Haddock Trac [http://trac.haskell.org/haddock/ticket/144 here] which I'm opening here as it requires lexer/parser changes. The idea is that given something like {{{ -- | A tree with labeled internal nodes data Tree = Empty -- ^ Leaf | Branch -- ^ Internal node { label :: a -- ^ Node label , subtrees :: [Tree] -- ^ List of subtrees } }}} we'd like it to parse as the user would expect instead of failing. We're currently forced to do something like {{{ -- | A tree with labeled internal nodes data Tree = Empty -- ^ Leaf | -- | Internal node Branch { label :: a -- ^ Node label , subtrees :: [Tree] -- ^ List of subtrees } }}} which is quite ugly. I can't think of a reason why the first form wouldn't be allowed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8822> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #9123: Need for higher kinded roles
by GHC 08 Jul '18

08 Jul '18

#9123: Need for higher kinded roles ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html thread] on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread {{{ class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a newtype T m a = MkT (m a) deriving( C ) }}} The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added. And the AMP proposal adds `join` to class `Monad`! In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used. This deficiency is noted in the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems to be the first occasion on which it has bitten us badly. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9123> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 66

[GHC] #9672: Error message too long (full case statement printed)
by GHC 06 Jul '18

06 Jul '18

#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

1 8