November 2015 - ghc-tickets

[GHC] #11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8
by GHC 10 Jul '18

10 Jul '18

#11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8 -------------------------------------+------------------------------------- Reporter: cactus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Given the following definitions (just a copy of the relevant bits from sized-types 0.3.5.1, to keep this example self-contained): {{{ -- Copied from sized-types 0.3.5.1 data X0 = X0 data N1 = N1 data X0_ a = X0_ Integer data X1_ a = X1_ Integer type X1 = X1_ X0 type X2 = X0_ (X1_ X0) class Size ix instance Size X0 instance Size a => Size (X1_ a) instance Size a => Size (X0_ a) type family APP0 a type instance APP0 X0 = X0 type instance APP0 N1 = X0_ N1 type instance APP0 (X1_ a) = X0_ (X1_ a) type instance APP0 (X0_ a) = X0_ (X0_ a) type family APP1 a type instance APP1 X0 = X1_ X0 type instance APP1 N1 = N1 type instance APP1 (X1_ a) = X1_ (X1_ a) type instance APP1 (X0_ a) = X1_ (X0_ a) type family SUCC a type instance SUCC X0 = X1_ X0 type instance SUCC N1 = X0 type instance SUCC (X1_ a) = APP0 (SUCC a) type instance SUCC (X0_ a) = APP1 a type family ADD a b type instance ADD a X0 = a type instance ADD X0 a = a type instance ADD X0 N1 = N1 type instance ADD N1 N1 = APP0 N1 type instance ADD N1 (X1_ b) = APP0 b type instance ADD N1 (X0_ b) = APP1 (ADD N1 b) type instance ADD (X1_ a) N1 = APP0 a type instance ADD (X0_ a) N1 = APP1 (ADD a N1) type instance ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b)) type instance ADD (X1_ a) (X0_ b) = APP1 (ADD a b) type instance ADD (X0_ a) (X1_ b) = APP1 (ADD a b) type instance ADD (X0_ a) (X0_ b) = APP0 (ADD a b) type family NOT a type instance NOT X0 = N1 type instance NOT N1 = X0 type instance NOT (X1_ a) = APP0 (NOT a) type instance NOT (X0_ a) = APP1 (NOT a) type SUB a b = ADD a (SUCC (NOT b)) }}} The following module typechecks with GHC 7.8.3: {{{ data B w = B (&*) :: (Size n, Size n', Size (ADD n' n), n ~ SUB (ADD n' n) n', n' ~ SUB (ADD n' n) n) => [(a, B n)] -> [(b, B n')] -> [((a, b), B (ADD n' n))] mks &* args = undefined foo :: [((), B X1)] foo = [((), B)] bar :: [(((), ()), B X2)] bar = [((), B)] &* foo }}} However, it fails with GHC 7.10.2, with {{{ /tmp/GHCBug.hs:70:7: Couldn't match type ‘ADD X1 n0’ with ‘X0_ (X1_ X0)’ The type variable ‘n0’ is ambiguous Expected type: [(((), ()), B X2)] Actual type: [(((), ()), B (ADD X1 n0))] In the expression: [((), B)] &* foo In an equation for ‘bar’: bar = [((), B)] &* foo /tmp/GHCBug.hs:70:17: Occurs check: cannot construct the infinite type: n0 ~ ADD (ADD X1 n0) N1 The type variable ‘n0’ is ambiguous Expected type: SUB (ADD X1 n0) X1 Actual type: n0 In the expression: [((), B)] &* foo In an equation for ‘bar’: bar = [((), B)] &* foo Failed, modules loaded: none. }}} The workaround/solution is to change the definition of `bar`: {{{ bar :: [(((), ()), B X2)] bar = [((), B :: B X1)] &* foo }}} This second version typechecks with GHC 7.10.2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11070> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[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

[GHC] #8263: allow duplicate deriving / standalone deriving
by GHC 04 Jul '18

04 Jul '18

#8263: allow duplicate deriving / standalone deriving ------------------------------------+------------------------------------- Reporter: aavogt | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- I would like to avoid conditional compilation. Currently I need to write: {{{ #if MIN_VERSION_Cabal(1,18,0) -- cabal 1.18 has these instances #else deriving instance Typeable Flag #endif }}} Would it be sane to have the deriving instance do nothing if the imported instance that clashes was also derived? reifyInstances together with a fixed #8100 could allow faking this feature. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8263> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #10391: Ability to get contents of TH reified module
by GHC 03 Jul '18

03 Jul '18

#10391: Ability to get contents of TH reified module -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature | Status: new request | Milestone: Priority: low | Version: Component: Template | Operating System: Unknown/Multiple Haskell | Type of failure: None/Unknown Keywords: | Blocked By: Architecture: | Related Tickets: Unknown/Multiple | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- After using reifyModule, I'd like to be able to inspect the list of exports from that module. At first I thought that this could perhaps be done by changing from {{{#!hs data ModuleInfo = -- | Contains the import list of the module. ModuleInfo [Module] }}} to {{{#!hs data ModuleInfo = -- | Contains the import list and export list of the module. ModuleInfo [Module] [Name] }}} but I now wonder if this is the best plan, because `thisModule >>= reifyModule` might be expected to function as a time machine, allowing us to see declarations that may not have been made yet (in the case where this module's export list is implicit). Can anyone propose a type that would allow us to perform this inspection for modules that have already been baked, but not for "this" module? An intended use case would be in our dimensional types library. We have several modules that define a whole bunch of units. It's useful for the unit name parser to have access to a dictionary with all of those units in it, but maintaining the definition of such a dictionary is redundant. If this feature existed, a module in the parser could import the modules where units are defined, examine the export lists, reify the names in the export lists, determine which represent unit definitions, and emit a declaration of a dictionary that contains them all. (This is in some ways similar to #9699, though perhaps more difficult?) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10391> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #8489: clean up dependency and usages handling in interface files
by GHC 02 Jul '18

02 Jul '18

#8489: clean up dependency and usages handling in interface files ----------------------------------------------+---------------------------- Reporter: errge | Owner: errge Type: task | Status: new Priority: normal | Milestone: 7.10.1 Component: Template Haskell | Version: 7.7 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Moderate (less than a day) | Type of failure: Blocked By: 1480 | None/Unknown Related Tickets: | Test Case: | Blocking: ----------------------------------------------+---------------------------- While reviewing #1480, it was found that there are corner cases that are not easy to handle. This task is about fixing TH module reification to reify direct import list, not usages. For this we may need to extend the current `ModIface`. This task also includes cleaning up the comments and code in related areas, to quote simonpj: "we need more precise commentary on the fields of `HscTypes.Dependencies`, `TcRnTypes.ImportAvails`, and `mi_usages` of `ModIface`. For example, I wonder whether the `mi_usages` field could be part of the `Dependencies`". -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8489> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 9

[GHC] #8695: Arithmetic overflow from (minBound :: Int) `quot` (-1)
by GHC 30 Jun '18

30 Jun '18

#8695: Arithmetic overflow from (minBound :: Int) `quot` (-1) -------------------------------------+------------------------------------- Reporter: rleslie | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: | Version: 7.6.3 libraries/haskell2010 | Operating System: Unknown/Multiple Keywords: | Type of failure: Incorrect result Architecture: Unknown/Multiple | at runtime Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- According to the documentation for Data.Int, “All arithmetic is performed modulo 2!^n, where n is the number of bits in the type.” However, this promise is broken by the following exception: {{{ Prelude> (minBound :: Int) `quot` (-1) *** Exception: arithmetic overflow }}} (This also occurs with Int8, Int16, Int32, and Int64, and likewise for `div`.) If all arithmetic is performed modulo 2!^n, I would rather expect the above to evaluate to `minBound`, since after all `minBound * (-1) == minBound`. The fact that an exception is raised adds an unnecessary burden in pure code to ensure `quot` (or `div`) is never called with these specific arguments. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8695> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 39

[GHC] #11024: Fix strange parsing of BooleanFormula
by GHC 29 Jun '18

29 Jun '18

#11024: Fix strange parsing of BooleanFormula -------------------------------------+------------------------------------- Reporter: mpickering | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.10.2 (Parser) | Keywords: newcomer | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following program. {{{ module Foo where class Meh a where foo :: a -> String foo1 :: a -> String foo2 :: a -> String {-# MINIMAL foo, foo1, foo2 #-} }}} The minimal pragma is parsed quite weirdly. {{{ (MinimalSig "{-# MINIMAL" (And [ (Var ({ test.hs:8:15-17 } (Unqual {OccName: foo}))), (And [ (Var ({ test.hs:8:20-23 } (Unqual {OccName: foo1}))), (Var ({ test.hs:8:26-29 } (Unqual {OccName: foo2})))])])))] {Bag(Located (HsBind RdrName)):}}} To be clear, it is parsed as `And [foo, [And [foo1, foo2]]` rather than `And [foo, foo1, foo2]`. Either the datatype should be change to be more like a binary tree or the parser should be changed to handle this properly. I think the second option would be easiest. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11024> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #9046: Panic in GHCi when using :print
by GHC 29 Jun '18

29 Jun '18

#9046: Panic in GHCi when using :print ------------------------------------+------------------------------------- Reporter: quchen | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.3 Component: GHCi | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: GHCi crash Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- When using names generated by :print, GHCi panics sometimes. According to #ghc, this is reproducible on ''x86_64-apple-darwin'' as well, but is not an issue in ''7.6.3 x86_64 linux''. {{{ > let a = [1] > :print a a = (_t1::Num t => [t]) > :t _t1 ghc: panic! (the 'impossible' happened) (GHC version 7.8.2 for x86_64-unknown-linux): tcTyVarDetails t{tv avD} [tv] > _t1 <same panic> }}} From playing around with it a bit, this seems to have something to do with polymorphic values. {{{ -- No panic > let a = [1 :: Int] > let a = 1 :: Int > let a = "hello" -- Panic > let a = [1] > let a = 1 > let a = "hello" -- With -XOverloadedStrings }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9046> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #10789: Notify user when a kind mismatch holds up a type family reduction
by GHC 28 Jun '18

28 Jun '18

#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- Consider this contrived example: {{{ {-# LANGUAGE TypeFamilies, PolyKinds, UndecidableInstances #-} module Bug where import Data.Proxy type family F (a :: k) :: k type instance F a = G a type family G a type instance G a = a foo :: Proxy (F Maybe) -> Proxy Maybe foo = id }}} This (correctly) fails to compile. The error message is {{{ Bug.hs:14:7: Couldn't match type ‘F Maybe’ with ‘Maybe’ Expected type: Proxy (F Maybe) -> Proxy Maybe Actual type: Proxy Maybe -> Proxy Maybe In the expression: id In an equation for ‘foo’: foo = id Failed, modules loaded: none. }}} But this is peculiar, but it surely looks like `F` should be a type-level identity function! Of course, upon further inspection, we see that `F` is partial. It reduces only at kind `*`. This is quite hard to figure out, though, especially given that we're using the "default to `*`" behavior of open type families to arrange for this kind restriction. Thus, I propose: figure out when a type family reduction is held up due to a kind mismatch, and inform the user. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10789> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15