- ghc-tickets - Haskell.org

[GHC] #15192: Refactor of Coercion
by GHC 21 Dec '18

21 Dec '18

#15192: Refactor of Coercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.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: -------------------------------------+------------------------------------- This patch aims at defining the new coercion rule {{{#!hs | EraseEqCo Role Type Type KindCoercion -- "e" -> _ -> _ -> N -> e }}} which corresponds to the typing rule {{{ t1 : k1 t2 : k2 |t1| = |t2| g : k1 ~ k2 ------------------------------------ EraseEqCo r t1 t2 g : t1 ~r t2 }}} Namely, if two types after erasure of casts and coercions are equivalent, then they can be casted from and to each other. This new coercion rule is designed to replace the current coherence rule {{{#!hs -- Coherence applies a coercion to the left-hand type of another coercion -- See Note [Coherence] | CoherenceCo Coercion KindCoercion -- :: e -> N -> e }}} The new rule is useful in several places. For example, now it is easier to define coercion {{{t |> k ~ t}}} without resorting to reflexivity coercion, and {{{t ~ t |> k}}} without resorting to symmetric rule. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15192> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 28

[GHC] #15113: Do not make CAFs from literal strings
by GHC 21 Dec '18

21 Dec '18

#15113: Do not make CAFs from literal strings -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.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: -------------------------------------+------------------------------------- Currently (as I discovered in #15038), we get the following code for `GHC.Exception.Base.patError`: {{{ lvl2_r3y3 :: [Char] [GblId] lvl2_r3y3 = unpackCString# lvl1_r3y2 -- RHS size: {terms: 7, types: 6, coercions: 2, joins: 0/0} patError :: forall a. Addr# -> a [GblId, Arity=1, Str=<B,U>x, Unf=OtherCon []] patError = \ (@ a_a2kh) (s_a1Pi :: Addr#) -> raise# @ SomeException @ 'LiftedRep @ a_a2kh (Control.Exception.Base.$fExceptionPatternMatchFail_$ctoException ((untangle s_a1Pi lvl2_r3y3) `cast` (Sym (Control.Exception.Base.N:PatternMatchFail[0]) :: (String :: *) ~R# (PatternMatchFail :: *)))) }}} That stupid `lvl2_r3y3 :: String` is a CAF, and hence `patError` has CAF- refs, and hence so does any function that calls `patError`, and any function that calls them. That's bad! Lots more CAF entries in SRTs, lots more work traversing those SRTs in the garbage collector. And for what? To share the work of unpacking a C string! This is nuts. What to do? * Somehow refrain from floating `unpackCSTring# lit` to top level, even if you could otherwise do so. But that seems very ad-hoc, and it make the function bigger and less inlinable. * Treat a top level definition {{{ x :: [Char] x = unpackCString# y }}} as NOT a CAF, and make it single-entry so that the thunk is not updated. Then every use of `x` will unpack the string afresh, which is probably a good idea anyhow. I like this more. It would be implemented somewhere in the code generator. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15113> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #16028: tyThingCoAxiom panics while building Agda
by GHC 21 Dec '18

21 Dec '18

#16028: tyThingCoAxiom panics while building Agda -------------------------------------+------------------------------------- Reporter: iliastsi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.4 Component: Compiler | Version: 8.4.4 Keywords: | Operating System: Unknown/Multiple Architecture: arm | Type of failure: Compile-time | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- ghc-8.4.4 panics while building Agda on armhf (https://buildd.debian.org/status/fetch.php?pkg=agda&arch=armhf&ver=2.5.4.1-…) {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.4.4 for arm-unknown-linux): tyThingCoAxiom Identifier ‘fromDescListWithKey’ Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable pprPanic, called at compiler/main/HscTypes.hs:2153:32 in ghc:HscTypes Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} The same version of Agda builds fine with ghc-8.4.3 on armhf (https://buildd.debian.org/status/fetch.php?pkg=agda&arch=armhf&ver=2.5.4.1-…) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16028> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #16065: Stack squeezing during context switches makes for non-determinism in allocations
by GHC 21 Dec '18

21 Dec '18

#16065: Stack squeezing during context switches makes for non-determinism in allocations -------------------------------------+------------------------------------- Reporter: sgraf | Owner: (none) Type: task | Status: new Priority: normal | Milestone: ⊥ Component: Runtime | Version: 8.6.3 System | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #4450, #8861 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- As #4450 and #8611 show, stack squeezing in the RTS makes allocation numbers between two different runs of the same binary non-deterministic, because its effect is depending on when context switches are bound to happen. A short-term solution might be to deactivate stack squeezing for vulnerable benchmarks with `+RTS -Z` like in Phab:D5460, but IMO a more elegant solution would be to only deactivate stack squeezing in `threadPause` calls that happen due to context switches. Would you agree? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16065> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #16076: Internal compiler error when instance uses FFI function and defining other instance of the same class through Template Haskell
by GHC 21 Dec '18

21 Dec '18

#16076: Internal compiler error when instance uses FFI function and defining other instance of the same class through Template Haskell -------------------------------------+------------------------------------- Reporter: | Owner: (none) radekchannable | Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.4 Keywords: | Operating System: Linux Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When one module defines an FFI function and uses it in an instance, and a Template Haskell function to derive an instance of the same class, using the function in another module causes GHC to crash, complaining it cannot find the FFI function. See the attached modules for an example. Use the following command to trigger the bug (ensure template-haskell is available): {{{ $ ghc Bar.hs [1 of 2] Compiling Foo ( Foo.hs, Foo.o ) [2 of 2] Compiling Bar ( Bar.hs, Bar.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.4.4 for x86_64-unknown-linux): Loading temp shared object failed: /tmp/ghc13955_0/libghc_6.so: undefined symbol: showFoo Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16076> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #16002: Type family equation with wrong name is silently accepted (GHC 8.6+ only)
by GHC 20 Dec '18

20 Dec '18

#16002: Type family equation with wrong name is silently accepted (GHC 8.6+ only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here's a program: {{{#!hs {-# LANGUAGE TypeFamilies #-} module TypeFamilies where data A type family B (x :: *) :: * where A x = x }}} One would hope that GHC would reject that nonsensical equation for `B` that references `A`. On GHC 7.8 through 8.4, that is the case: {{{ $ /opt/ghc/8.4.4/bin/ghci Bug.hs GHCi, version 8.4.4: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling TypeFamilies ( Bug.hs, interpreted ) Bug.hs:6:3: error: • Mismatched type name in type family instance. Expected: B Actual: A • In the type family declaration for ‘B’ | 6 | A x = x | ^^^^^^^ }}} But GHC 8.6.2 and HEAD actually //accept// this program! Thankfully, GHC appears to just treat `A x = x` as though you had written `B x = x`, so it's not like this breaks type safety or anything. Still, this most definitely ought to be rejected. One interesting observation is that `B` having a CUSK appears to be important. If `B` doesn't have a CUSK, as in the following variant: {{{#!hs {-# LANGUAGE TypeFamilies #-} module TypeFamilies where data A type family B x where A x = x }}} Then GHC properly catches the mismatched use of `A`: {{{ $ /opt/ghc/8.6.2/bin/ghci Bug.hs GHCi, version 8.6.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling TypeFamilies ( Bug.hs, interpreted ) Bug.hs:6:3: error: • Mismatched type name in type family instance. Expected: B Actual: A • In the type family declaration for ‘B’ | 6 | A x = x | ^^^^^^^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16002> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #15577: TypeApplications-related infinite loop (GHC 8.6+ only)
by GHC 20 Dec '18

20 Dec '18

#15577: TypeApplications-related infinite loop (GHC 8.6+ only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple TypeApplications, TypeInType | Architecture: | Type of failure: Compile-time Unknown/Multiple | performance bug Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program will loop infinitely when compiled on GHC 8.6 or HEAD: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Type.Equality data family Sing :: forall k. k -> Type class Generic1 (f :: k -> Type) where type Rep1 f :: k -> Type class PGeneric1 (f :: k -> Type) where type From1 (z :: f a) :: Rep1 f a type To1 (z :: Rep1 f a) :: f a class SGeneric1 (f :: k -> Type) where sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z) sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a) class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where sTof1 :: forall (a :: k) (z :: f a). Sing z -> To1 (From1 z) :~: z sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r foo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a). VGeneric1 f => Sing r -> From1 (To1 r :: f a) :~: r foo x | Refl <- sFot1 -- Uncommenting the line below makes it work again: -- @Type @f @a @r x = Refl }}} This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors: {{{ $ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:35:20: error: • Expecting one more argument to ‘f’ Expected a type, but ‘f’ has kind ‘* -> *’ • In the type ‘f’ In a stmt of a pattern guard for an equation for ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl | 35 | @f @a @r x | ^ Bug.hs:35:23: error: • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’ • In the type ‘a’ In a stmt of a pattern guard for an equation for ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 35 | @f @a @r x | ^ Bug.hs:35:26: error: • Couldn't match kind ‘* -> *’ with ‘*’ When matching kinds f1 :: * -> * Rep1 f1 a1 :: * Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’ • In the type ‘r’ In a stmt of a pattern guard for an equation for ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 35 | @f @a @r x | ^ Bug.hs:35:28: error: • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’ When matching kinds a1 :: * 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep • In the fourth argument of ‘sFot1’, namely ‘x’ In a stmt of a pattern guard for an equation for ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 35 | @f @a @r x | ^ Bug.hs:36:5: error: • Could not deduce: From1 (To1 r1) ~ r1 from the context: r0 ~ From1 (To1 r0) bound by a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in a pattern binding in pattern guard for an equation for ‘foo’ at Bug.hs:33:5-8 ‘r1’ is a rigid type variable bound by the type signature for: foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1). VGeneric1 f1 => Sing r1 -> From1 (To1 r1) :~: r1 at Bug.hs:(29,1)-(31,43) Expected type: From1 (To1 r1) :~: r1 Actual type: r1 :~: r1 • In the expression: Refl In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 36 | = Refl | ^^^^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15577> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #16074: Hopelessly confusing error involving runtime-reps
by GHC 20 Dec '18

20 Dec '18

#16074: Hopelessly confusing error involving runtime-reps -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 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: -------------------------------------+------------------------------------- Consider {{{ {-# LANGUAGE GADTs, TypeOperators, PolyKinds #-} import GHC.Types data a :~: b where Refl :: a :~: a foo :: TYPE a :~: TYPE b foo = Refl }}} We get {{{ • Couldn't match type ‘'LiftedRep’ with ‘'LiftedRep’ ‘a’ is a rigid type variable bound by the type signature for: foo :: * :~: * at Repr.hs:7:1-24 ‘b’ is a rigid type variable bound by the type signature for: foo :: * :~: * at Repr.hs:7:1-24 }}} That's a ridiculous message. But if you asdd `-fprint-explicit-runtime- reps` we get {{{ • Couldn't match type ‘a’ with ‘b’ ‘a’ is a rigid type variable bound by the type signature for: foo :: forall (a :: RuntimeRep) (b :: RuntimeRep). TYPE a :~: TYPE b at T16050.hs:9:1-24 ‘b’ is a rigid type variable bound by the type signature for: foo :: forall (a :: RuntimeRep) (b :: RuntimeRep). TYPE a :~: TYPE b at T16050.hs:9:1-24 Expected type: TYPE a :~: TYPE b Actual type: TYPE a :~: TYPE a • In the expression: Refl In an equation for ‘foo’: foo = Refl • Relevant bindings include foo :: TYPE a :~: TYPE b (bound at T16050.hs:10:1) }}} which is the right error. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16074> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #16033: Rank-n typechecking regression between GHC 8.4 and 8.6
by GHC 20 Dec '18

20 Dec '18

#16033: Rank-n typechecking regression between GHC 8.4 and 8.6 -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.3 (Type checker) | Keywords: RankNTypes | 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: -------------------------------------+------------------------------------- The following program typechecks on GHC 7.0.4 through 8.4.4: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where f :: (forall a. a -> forall b. b -> c) -> () f (_ :: forall a. a -> forall b. b -> z) = () }}} However, it does not typecheck on GHC 8.6.3: {{{ $ /opt/ghc/8.6.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:7:4: error: • Couldn't match type ‘b0 -> c’ with ‘forall b. b -> z’ Expected type: a -> forall b. b -> z Actual type: a -> b0 -> c • When checking that the pattern signature: forall a. a -> forall b. b -> z fits the type of its context: forall a. a -> forall b. b -> c In the pattern: _ :: forall a. a -> forall b. b -> z In an equation for ‘f’: f (_ :: forall a. a -> forall b. b -> z) = () • Relevant bindings include f :: (forall a. a -> forall b. b -> c) -> () (bound at Bug.hs:7:1) | 7 | f (_ :: forall a. a -> forall b. b -> z) = () | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16033> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #16030: Poor pretty-printing of GADT constructors in GHCi
by GHC 20 Dec '18

20 Dec '18

#16030: Poor pretty-printing of GADT constructors in GHCi -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 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: -------------------------------------+------------------------------------- I recently loaded this file into GHCi: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Proxy data Foo1 (a :: k) where MkFoo1a :: Proxy a -> Int -> Foo1 a MkFoo1b :: { a :: Proxy a, b :: Int } -> Foo1 a data family Foo2 (a :: k) data instance Foo2 (a :: k) where MkFoo2a :: Proxy a -> Int -> Foo2 a MkFoo2b :: { c :: Proxy a, d :: Int} -> Foo2 a }}} And when I queried these datatypes with `:info`, I saw this: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs -fprint- explicit-kinds GHCi, version 8.7.20181129: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Ok, one module loaded. λ> :i Foo1 Foo2 type role Foo1 nominal phantom data Foo1 @k (a :: k) where MkFoo1a :: forall k (a :: k). (Proxy @{k} a) -> Int -> Foo1 k a MkFoo1b :: forall k (a :: k). {a :: Proxy @{k} a, b :: Int} -> Foo1 k a -- Defined at Bug.hs:8:1 data family Foo2 @k (a :: k) -- Defined at Bug.hs:12:1 data instance forall k (a :: k). Foo2 @k a where MkFoo2a :: forall k (a :: k). (Proxy @{k} a) -> Int -> Foo2 @k a MkFoo2b :: forall k (a :: k). {c :: Proxy @{k} a, d :: Int} -> Foo2 @k a -- Defined at Bug.hs:13:15 }}} Yuck. A couple of icky things to note here: * For some reason, the `Proxy @{k} a` field is needlessly parenthesized in `MkFoo1a` and `MkFoo2a`. This does //not// happen when record syntax is used, as demonstrated with `MkFoo1b` and `MkFoo2b`. * Even more strangely, despite the fact that `k` is a specified argument, we're pretty-printing the return type of `MkFoo1{a,b}` as `Foo k a`, not `Foo @k a`. This problem doesn't appear to happen for data family instances, since `MkFoo2{a,b}` don't have this issue. Patch incoming. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16030> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6