July 2018 - ghc-tickets

[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

Re: [GHC] #1311: newtypes of unboxed types disallowed - documentation bug and/or feature request
by GHC 08 Jul '18

08 Jul '18

#1311: newtypes of unboxed types disallowed - documentation bug and/or feature request -------------------------------------+------------------------------------- Reporter: Isaac Dupree | Owner: osa1 Type: feature request | Status: patch Priority: low | Milestone: ⊥ Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15219 | Differential Rev(s): Phab:D4777 Wiki Page: | -------------------------------------+------------------------------------- Changes (by osa1): * status: new => patch * differential: => Phab:D4777 * related: => #15219 Comment: The [https://github.com/ghc-proposals/ghc- proposals/blob/master/proposals/0013-unlifted-newtypes.rst proposal] was accepted and this feature is currently being implemented. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/1311#comment:22> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #2189: hSetBuffering stdin NoBuffering doesn't work on Windows
by GHC 07 Jul '18

07 Jul '18

#2189: hSetBuffering stdin NoBuffering doesn't work on Windows -------------------------------------+------------------------------------- Reporter: FalconNL | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 6.8.2 Resolution: | Keywords: hsetbuffering | buffering buffer Operating System: Windows | Architecture: x86 Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11394, #13440 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Phyx-): OK, this now works with the new Windows I/O manager. Hopefully included in 8.8. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/2189#comment:53> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[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] #12073: Missing instance of MonadFix for Q
by GHC 06 Jul '18

06 Jul '18

#12073: Missing instance of MonadFix for Q -------------------------------------+------------------------------------- Reporter: jophish | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Template | Version: Haskell | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- `Q` is capable of being an instance of `MonadFix`. The definition of `mfix` is the same as `fixIO` except that the `MVar` handling is wrapped in `runIO`. {{{#!hs instance MonadFix Q where mfix k = do m <- runIO newEmptyMVar ans <- runIO (unsafeInterleaveIO (takeMVar m)) result <- k ans runIO (putMVar m result) pure result }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12073> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #14470: CircleCI: Detect number of processors
by GHC 06 Jul '18

06 Jul '18

#14470: CircleCI: Detect number of processors -------------------------------------+------------------------------------- Reporter: bgamari | Owner: bgamari Type: task | Status: new Priority: normal | Milestone: Component: Continuous | Version: 8.2.1 Integration | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Currently we hard-code the thread count to 8, which is what the machines which jobs from the `ghc/ghc` repository run on. However, such machines are not available to owners of `ghc` forks (unless they specifically request a resource limit bump from CircleCI). We should automatically detect the CPU count to ensure that CI on smaller instances will not fail due to oversubscription. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14470> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #14083: ?
by GHC 06 Jul '18

06 Jul '18

#14083: ? -------------------------------------+------------------------------------- Reporter: zaoqi | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} class GEq a b where geq :: a -> b -> Bool instance {-# OVERLAPPABLE #-} (Eq a) => GEq a a where geq = (==) instance {-# OVERLAPPING #-} GEq a b where geq _ _ = False }}} {{{ GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Prelude> :load GEq.hs [1 of 1] Compiling Main ( GEq.hs, interpreted ) Ok, modules loaded: Main. *Main> geq () () <interactive>:2:1: error: • Overlapping instances for GEq () () arising from a use of ‘geq’ Matching instances: instance [overlapping] [safe] GEq a b -- Defined at GEq.hs:9:30 instance [overlappable] [safe] Eq a => GEq a a -- Defined at GEq.hs:6:31 • In the expression: geq () () In an equation for ‘it’: it = geq () () *Main> }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14083> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[GHC] #11523: Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.
by GHC 05 Jul '18

05 Jul '18

#11523: Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.3 (Type checker) | Keywords: | Operating System: Unknown/Multiple UndecidableSuperClasses | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: #11480 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- There seems to be a bad interaction between `UndecidableSuperClasses` and the common trick of using a cyclic definition of a class and instance to make an alias at the constraint level: {{{#!hs class (Foo f, Bar f) => Baz f instance (Foo f, Bar f) => Baz f }}} Unfortunately, there are circumstances in which you can't eliminate it, such as {{{#!hs class (p, q) => p & q instance (p, q) => p & q }}} There we can't partially apply (,) at the constraint level, but we can talk about `(&) :: Constraint -> Constraint -> Constraint` and `(&) (Eq a) :: Constraint -> Constraint`. This doesn't seem to happen on simpler examples like the above, but once I modify the categories example from #11480 to move the domain and codomain of a functor into class associated types, so that they don't infect every single subclass of functor, we run into a problem. The following stripped down version of the code seems to send the compiler into an infinite loop: {{{#!hs {-# language KindSignatures #-} {-# language PolyKinds #-} {-# language DataKinds #-} {-# language TypeFamilies #-} {-# language RankNTypes #-} {-# language NoImplicitPrelude #-} {-# language FlexibleContexts #-} {-# language MultiParamTypeClasses #-} {-# language GADTs #-} {-# language ConstraintKinds #-} {-# language FlexibleInstances #-} {-# language TypeOperators #-} {-# language ScopedTypeVariables #-} {-# language DefaultSignatures #-} {-# language FunctionalDependencies #-} {-# language UndecidableSuperClasses #-} {-# language UndecidableInstances #-} {-# language TypeInType #-} import GHC.Types (Constraint, Type) import qualified Prelude type Cat i = i -> i -> Type newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a } class Vacuous (a :: i) instance Vacuous a class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where type Op p :: Cat i type Op p = Y p type Ob p :: i -> Constraint type Ob p = Vacuous class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where type Dom f :: Cat i type Cod f :: Cat j class (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q instance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = Fun p q instance (Category p, Category q) => Functor (Nat p q) where type Dom (Nat p q) = Y (Nat p q) type Cod (Nat p q) = Nat (Nat p q) (->) instance (Category p, Category q) => Functor (Nat p q f) where type Dom (Nat p q f) = Nat p q type Cod (Nat p q f) = (->) instance Category (->) instance Functor ((->) e) where type Dom ((->) e) = (->) type Cod ((->) e) = (->) instance Functor (->) where type Dom (->) = Y (->) type Cod (->) = Nat (->) (->) instance (Category p, Op p ~ Y p) => Category (Y p) where type Op (Y p) = p instance (Category p, Op p ~ Y p) => Functor (Y p a) where type Dom (Y p a) = Y p type Cod (Y p a) = (->) instance (Category p, Op p ~ Y p) => Functor (Y p) where type Dom (Y p) = p type Cod (Y p) = Nat (Y p) (->) }}} Here I need the circular definition of `Fun` to talk about the fact that the objects in the category of natural transformations from a category p to a category q are functors with domain p and codomain q, so to give the definition of the class-associated `type Ob (Nat p q)` I need such a cyclic definition. I can't leave the domain and codomain of `Functor` in fundeps, otherwise if I go to define a subclass of Functor I'd have to include the arguments, and I have a ''lot'' of those subclasses! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11523> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 33

[GHC] #15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints
by GHC 05 Jul '18

05 Jul '18

#15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this program: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE QuantifiedConstraints #-} module Bug where import Data.Kind data ECC :: Constraint -> Type -> Type class Y a class Z a instance c => Y (ECC c a) instance (c => Z a) => Z (ECC c a) }}} I would expect both of these instances to work. But while GHC accepts the `Y` instance, it rejects the `Z` instance: {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:10: error: • Variable ‘c’ occurs more often in the constraint ‘c’ than in the instance head (Use UndecidableInstances to permit this) • In the instance declaration for ‘Z (ECC c a)’ | 15 | instance (c => Z a) => Z (ECC c a) | ^^^^^^^^^^^^^^^^^^^^^^^^^ }}} That error message seems completely bogus to me, since `c` appears once in both the context and instance head in both instances. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15231> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #14883: QuantifiedConstraints don't kick in when used in TypeApplications
by GHC 05 Jul '18

05 Jul '18

#14883: QuantifiedConstraints don't kick in when used in TypeApplications -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following program: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Bug where import Data.Coerce import Data.Kind type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint) class Representational1 f => Functor' f where fmap' :: (a -> b) -> f a -> f b class Functor' f => Applicative' f where pure' :: a -> f a (<*>@) :: f (a -> b) -> f a -> f b class Functor' t => Traversable' t where traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b) -- Typechecks newtype T1 m a = MkT1 (m a) deriving Functor' instance Traversable' m => Traversable' (T1 m) where traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f (T1 m b) traverse' = coerce @((a -> f b) -> m a -> f (m b)) @((a -> f b) -> T1 m a -> f (T1 m b)) traverse' -- Doesn't typecheck newtype T2 m a = MkT2 (m a) deriving Functor' instance Traversable' m => Traversable' (T2 m) where traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b)) @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b)) traverse' }}} This defines a variant of `Functor` that has `forall a b. Coercible a b. Coercible (m a) (m b)` as a superclass, and also defines versions of `Applicative` and `Traversable` that use this `Functor` variant. This is towards the ultimate goal of defining `Traversable'` à la `GeneralizedNewtypeDeriving`. This attempt (using `InstanceSigs`) typechecks: {{{#!hs newtype T1 m a = MkT1 (m a) deriving Functor' instance Traversable' m => Traversable' (T1 m) where traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f (T1 m b) traverse' = coerce @((a -> f b) -> m a -> f (m b)) @((a -> f b) -> T1 m a -> f (T1 m b)) traverse' }}} However, this version (which is closer to what `GeneralizedNewtypeDeriving` would actually create) does //not// typecheck: {{{#!hs newtype T2 m a = MkT2 (m a) deriving Functor' instance Traversable' m => Traversable' (T2 m) where traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b)) @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b)) traverse' }}} {{{ $ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:38:15: error: • Couldn't match representation of type ‘f1 (m b1)’ with that of ‘f1 (T2 m b1)’ arising from a use of ‘coerce’ NB: We cannot know what roles the parameters to ‘f1’ have; we must assume that the role is nominal • In the expression: coerce @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b)) @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b)) traverse' In an equation for ‘traverse'’: traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b)) @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b)) traverse' In the instance declaration for ‘Traversable' (T2 m)’ • Relevant bindings include traverse' :: (a -> f b) -> T2 m a -> f (T2 m b) (bound at Bug.hs:38:3) | 38 | traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b)) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... }}} Shouldn't it, though? These instance declarations out to be equivalent (morally, at least). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14883> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10