September 2018 - ghc-tickets

[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] #15635: Implication introduction for quantified constraints
by GHC 29 Nov '18

29 Nov '18

#15635: Implication introduction for quantified constraints -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types: {{{#!hs data Dict a where Dict :: a => Dict a newtype a :- b = Sub (a => Dict b) }}} `QuantifiedConstraints` suggests another version of `:-`: {{{#!hs newtype Imp a b = Imp { unImp :: forall r. ((a => b) => r) -> r} }}} We can write {{{#!hs fromImp :: Imp a b -> a :- b fromImp (Imp f) = Sub (f Dict) }}} But ... there's no way to go the other way! Let's try it: {{{#!hs toImp :: a :- Dict b -> a :- b toImp (Sub ab) = Imp $ \r -> _ }}} We get {{{ * Found hole: _ :: r * Relevant bindings include r :: (a => b) => r ab :: a => Dict b }}} There's no way to put these things together. But there's no terribly obvious reason they ''can't'' be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that ''contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic: {{{#!hs implIntro :: ((a => b) => q) -> (forall r. (b => r) -> (a => r)) -> q }}} In Core (modulo type abstraction and application), we could simply write {{{#!hs implIntro f g = f (g id) }}} Unfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15635> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[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] #15414: Why both gen and gen_no in bdescr?
by GHC 29 Nov '18

29 Nov '18

#15414: Why both gen and gen_no in bdescr? -------------------------------------+------------------------------------- Reporter: bgamari | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.1 Component: Runtime | Version: 8.4.3 System | 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: -------------------------------------+------------------------------------- Block descriptors currently contain both `gen` (a `generation *`) and `gen_no` (a `uint16_t, which is `gen->no` cached). I wonder whether it would be worthwhile to drop the former and always use `generations[bd->gen_no]`. Afterall, this would save an entire word per descriptor which may improve our caches' coverage of the bdescr region appreciably. Presumably the `generations` array would be hot enough to stay in cache in such a scheme, so I would guess that the cost would be small-ish. Simon, have you measured this in the past? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15414> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[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] #15293: Set up staging branch
by GHC 28 Nov '18

28 Nov '18

#15293: Set up staging branch -------------------------------------+------------------------------------- Reporter: bgamari | Owner: bgamari Type: task | Status: new Priority: highest | Milestone: 8.6.1 Component: Continuous | Version: 8.4.3 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: -------------------------------------+------------------------------------- Goal: Keep commits that would break CI out of `master`. Approach: Introduce a staging branch where commits will first land to go through the full CI workup. When a commit passes on `staging`, merge it into `master`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15293> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[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