April 2018 - ghc-tickets

[GHC] #14230: Gruesome kind mismatch errors for associated data family instances
by GHC 30 Nov '18

30 Nov '18

#14230: Gruesome kind mismatch errors for associated data family instances -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: #14175 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Spun off from https://ghc.haskell.org/trac/ghc/ticket/14175#comment:9. This program, which can only really be compiled on GHC HEAD at the moment: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module Bug where class C k where data CD :: k -> k -> * instance C (Maybe a) where data CD :: (k -> *) -> (k -> *) -> * }}} Gives a heinous error message: {{{ Bug.hs:11:3: error: • Expected kind ‘(k -> *) -> (k -> *) -> *’, but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a -> Maybe a -> *’ • In the data instance declaration for ‘CD’ In the instance declaration for ‘C (Maybe a)’ | 11 | data CD :: (k -> *) -> (k -> *) -> * | ^^^^^^^ }}} * We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself. * The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`. Another program in a similar vein: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C a where data CD k (a :: k) :: k -> * instance C (Maybe a) where data CD k (a :: k -> *) :: (k -> *) -> * }}} {{{ Bug.hs:13:3: error: • Expected kind ‘(k -> *) -> *’, but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’ • In the data instance declaration for ‘CD’ In the instance declaration for ‘C (Maybe a)’ | 13 | data CD k (a :: k -> *) :: (k -> *) -> * | ^^^^^^^^^^^^^^^^^^^^^^^ }}} This error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14230> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #13492: -p option report much less time than actual on high intensity of FFI calls application
by GHC 30 Nov '18

30 Nov '18

#13492: -p option report much less time than actual on high intensity of FFI calls application -------------------------------------+------------------------------------- Reporter: varosi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Profiling | Version: 8.0.2 Keywords: | Operating System: Windows Architecture: x86_64 | Type of failure: Debugging (amd64) | information is incorrect Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Proprietary application is ran on 44 cores (88 with HT) machine (same problem on 12 core). It is Haskell between wxHaskell (wxWidgets for UI) and C API. It is doing FFI calls most of the time. Calls are not so many, but possibly not so fast. I'm trying to profile where is the problem, in which calls. But very strange behaviour is there. "total time" of application that is running 30secs to 1min is showing 0.33secs. Even MAIN function is not 100%. Please, see first part of .prof file: Tue Mar 28 15:38 2017 Time and Allocation Profiling Report (Final) app.exe +RTS -N -A40m -qb0 -p -RTS total time = 0.33 secs (325 ticks @ 1000 us, 1 processor) total alloc = 86,317,264 bytes (excludes profiling overheads) COST CENTRE MODULE SRC %time %alloc MAIN MAIN <built- in> 12.6 2.2 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13492> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #14937: QuantifiedConstraints: Reify implication constraints from terms lacking them
by GHC 29 Nov '18

29 Nov '18

#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #14822 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is possibly the same question as #14822, asked in more general terms. Would it be viable/sound to have a way of extracting implication constraints out of terms which effectively encode such constraints, such as `(:-)` from `Data.Constraint`? Here's how I think about it. `a :- b` is equivalent to `forall r. a => (b => r) -> r`. This is a type that, as I read it, expresses "if you can show `a`, then I can show `b`". This is very similar to `forall r. ((a => b) => r) -> r`, which expresses "(without obligations) I can show that `a` implies `b`". It seems to me (and I know this is hand-wavy) like expressions of both of these types actually must have the same "knowledge", i.e. that `a` imples `b`. Is this actually correct? I am wondering whether we could have a built-in function like: {{{#!hs reifyImplication :: forall a b. (forall r. a => (b => r) -> r) -> (forall r. ((a => b) => r) -> r) }}} We can already write the function that goes the other direction. There are plenty of ways to represent this conversion. Some more straight- forward, using `a :- b` or `Dict a -> Dict b`. I just went with one that doesn't require any types beyond arrows. I'm curious about the soundness of this. I have tried really hard to implement this function, but I don't think it can be done. I don't know if this proves anything, but replacing `(=>)` with `(->)` and all constraints `c` with `Dict c`, this function can be written: {{{#!hs dictReifyImplication :: forall a b. (forall r. Dict a -> (Dict b -> r) -> r) -> (forall r. ((Dict a -> Dict b) -> r) -> r) dictReifyImplication f g = g (\a -> f a id) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14937> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #14887: Explicitly quantifying a kind variable causes a type family to fail to typecheck
by GHC 29 Nov '18

29 Nov '18

#14887: Explicitly quantifying a kind variable causes a type family to fail to typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: TypeFamilies, | Operating System: Unknown/Multiple TypeInType | 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 TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fprint-explicit-kinds #-} module Bug where import Data.Kind import Data.Type.Equality type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where Foo1 (e :: a :~: a) = a :~: a type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where Foo2 k (e :: a :~: a) = a :~: a }}} `Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not! {{{ $ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:13:10: error: • Couldn't match kind ‘k’ with ‘k1’ When matching the kind of ‘a’ Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’ • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’ In the type family declaration for ‘Foo2’ | 13 | Foo2 k (e :: a :~: a) = a :~: a | ^^^^^^^^^^^^^^ }}} (Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14887> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15

[GHC] #14880: GHC panic: updateRole
by GHC 29 Nov '18

29 Nov '18

#14880: GHC panic: updateRole -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: Roles | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Type.Equality ((:~:)(..)) type SameKind (a :: k) (b :: k) = (() :: Constraint) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type f @@ x = f `Apply` x infixl 9 @@ type family WhyCong (x :: Type) (y :: Type) (f :: x ~> y) (a :: x) (z :: x) (e :: a :~: z) :: Type where WhyCong _ _ f a z _ = f @@ a :~: f @@ z data WhyCongSym1 (x :: Type) :: forall (a :: x) (y :: Type) (z :: x). Type ~> (x ~> y) ~> x ~> x ~> a :~: z ~> Type data WhyCongSym0 :: forall (x :: Type) (a :: x) (y :: Type) (z :: x). Type ~> Type ~> (x ~> y) ~> x ~> x ~> a :~: z ~> Type where WhyCongSym0KindInference :: forall x arg. SameKind (Apply WhyCongSym0 arg) (WhyCongSym1 arg) => WhyCongSym0 x }}} {{{ $ /opt/ghc/8.2.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.2.2 for x86_64-unknown-linux): updateRole WhyCongSym0 arg_aYV[sk:1] [aYU :-> 4, a22o :-> 0, a22p :-> 1, a22q :-> 2, a22r :-> 3] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14880> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 160

[GHC] #8177: Roles for type families
by GHC 29 Nov '18

29 Nov '18

#8177: Roles for type families ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | 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: | ------------------------------------+------------------------------------- Now that we have [wiki:Roles roles], it might be helpful to be able to give a role signature for a data/type family. At the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus {{{ data family D a -- Parameter conservatively assumed to be N class C a where op :: D a -> a instance C Int where .... newtype N a = MkN a deriving( C ) -- Rejected }}} The generalised-newtype-deriving clause `deriving( C )` is rejected because `D` might use its parameter at role `N` thus: {{{ data instance D [b] = MkD (F b) -- F is a type function }}} It would be strictly more expressive if we could * '''Declare''' the roles of D's arguments (as we can declare their kinds). E.g. {{{ data family D a@R }}} * '''Check''' that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance: {{{ data instance D [b] = MkD (F b) -- F is a type function }}} I think there is no technical difficulty here. Just a question of doing it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8177> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 41

[GHC] #14506: Configure Harbormaster to trigger CircleCI commits
by GHC 28 Nov '18

28 Nov '18

#14506: Configure Harbormaster to trigger CircleCI commits -------------------------------------+------------------------------------- Reporter: bgamari | Owner: bgamari Type: bug | 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: -------------------------------------+------------------------------------- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14506> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 9

[GHC] #14950: GHC 8.2.2: GHCi duplicates breakpoint range prompt
by GHC 28 Nov '18

28 Nov '18

#14950: GHC 8.2.2: GHCi duplicates breakpoint range prompt -------------------------------------+------------------------------------- Reporter: lierdakil | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Other Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I think breakpoint range is being printed twice, once as part of prompt, and the second time by itself. To reproduce, create `test.hs` file like this: {{{#!hs module Test where test :: IO () test = putStrLn "Hello, World!" }}} Then run the following GHCi session: {{{ $ ghci test.hs GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Test ( test.hs, interpreted ) Ok, one module loaded. *Test> :break test Breakpoint 0 activated at test.hs:4:8-31 *Test> :trace test Stopped in Test.test, test.hs:4:8-31 _result :: IO () = _ [test.hs:4:8-31] [test.hs:4:8-31] *Test> :set prompt "" [test.hs:4:8-31] }}} Notice `[test.hs:4:8-31]` is printed twice, and is even printed when prompt is set to `""`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14950> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[GHC] #12965: String merging broken on Windows
by GHC 26 Nov '18

26 Nov '18

#12965: String merging broken on Windows ----------------------------------------+--------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Windows Architecture: Unknown/Multiple | Type of failure: None/Unknown Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: ----------------------------------------+--------------------------------- #9577 introduced string literal merging via the linker. Unfortunately I haven't been able to get this to function on Windows, resulting in testsuite failures of #9577. Even `gcc` appears to do the wrong thing here, {{{ $ cat hi.c #include <stdio.h> const char *hi = "hello world"; extern const char *hi2; void main() { printf("%p %p", hi, hi2); } $ cat hi2.c const char *hi2 = "hello world"; $ gcc -c hi.c; gcc -c hi2.c; gcc -fmerge-all-constants hi2.o hi.o $ ./a.exe 0x100403040 0x100403030 $ gcc -s hi2.c $ cat hi2.s .file "hi2.c" .globl hi .section .rdata,"dr" .LC0: .ascii "hello world\0" .data .align 8 hi: .quad .LC0 .ident "GCC: (GNU) 5.3.0" }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12965> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #14482: GHC -M mode fails to ensure that boot files are built before source files
by GHC 26 Nov '18

26 Nov '18

#14482: GHC -M mode fails to ensure that boot files are built before source files -------------------------------------+------------------------------------- Reporter: bgamari | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 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: -------------------------------------+------------------------------------- Imagine we have a module with a boot file. In general it is necessary to ensure that we compile the boot file *before* the source file to ensure that the `hi-boot` file exists when we go to typecheck the module (triggering the behavior observed in #14481). However, `ghc -M` doesn't guarantee this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14482> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7