September 2016 - ghc-tickets

[GHC] #12119: Can't create injective type family equation with TypeError as the RHS
by GHC 24 Oct '18

24 Oct '18

#12119: Can't create injective type family equation with TypeError as the RHS -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple CustomTypeErrors, TypeFamilies, | Injective | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- For the longest time, I've wanted to make a type family like this injective: {{{#!hs type family Foo (a :: *) :: * where Foo Bar = Int Foo Baz = Char }}} But the problem is that `Foo` is defined on //all// types of kind `*`, so the above definition is inherently non-injective. With the introduction of `TypeError`s, however, I thought I could rule out all other cases: {{{#!hs import GHC.TypeLits type family Foo (a :: *) = (r :: *) | r -> a where Foo Bar = Int Foo Baz = Char Foo _ = TypeError ('Text "boom") }}} But this doesn't work, sadly: {{{ Injective.hs:18:3: error: • Type family equations violate injectivity annotation: Foo Bar = Int -- Defined at Injective.hs:18:3 Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3 • In the equations for closed type family ‘Foo’ In the type family declaration for ‘Foo’ Injective.hs:20:3: error: • Type family equation violates injectivity annotation. Type variable ‘_’ cannot be inferred from the right-hand side. In the type family equation: Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3 • In the equations for closed type family ‘Foo’ In the type family declaration for ‘Foo’ Injective.hs:20:3: error: • Type family equation violates injectivity annotation. RHS of injective type family equation cannot be a type family: Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3 • In the equations for closed type family ‘Foo’ In the type family declaration for ‘Foo’ }}} From GHC's perspective, `TypeError` is just another type family, so it thinks it violates injectivity. But should this be the case? After all, having the RHS of a type family equation being `TypeError` is, in my perspective, tantamount to making that type family undefined for those inputs. It seems like if we successfully conclude that `Foo a ~ Foo b` (and GHC hasn't blown up yet due to type erroring), we should be able to conclude that `a ~ b`. Could this be accomplished by simply adding a special case for `TypeError` in the injectivity checker? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12119> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #11307: Regresssion: parsing type operators
by GHC 17 Oct '18

17 Oct '18

#11307: Regresssion: parsing type operators -------------------------------------+------------------------------------- Reporter: alanz | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.11 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: -------------------------------------+------------------------------------- GHC 7.10.3 will parse (but not type-check) the following {{{#!hs {-# LANGUAGE TypeOperators #-} type family (r1 :++: r2); infixr 5 :++: type instance r :++: Nil = r type instance r1 :++: r2 :> a = (r1 :++: r2) :> a }}} Current master (c7830bdb14e0a85a78617314156d101155fdf7aa) fails with {{{#!hs /tmp/Foo.hs:5:15: error: Malformed head of type or class declaration: r1 :++: r2 :> a }}} @simonpj comment on ghc-devs mailing list > `| type instance r1 :++: r2 :> a = (r1 :++: r2) :> a` > > What do you expect this to mean? I suppose you could hope that GHC will > unravel the fixity of :++: and :>, to determine whether you are giving an > instance for :++: or for :>? > > That sounds reasonable, but it's not trivial. > > Currently the LHS of a 'type instance' decl is ultimately a TyFamEqn, and > it looks like this: > > {{{#!hs > data TyFamEqn name pats > = TyFamEqn > { tfe_tycon :: Located name > , tfe_pats :: pats > , tfe_rhs :: LHsType name } > }}} > > So we've already decided (in the parser) what the type-function name is. > But we can't do that in this case, because the parser doesn't understand > fixity. > > To deal with this we'd need to change to > > {{{#!hs > data TyFamEqn name pats > = TyFamEqn > { tfe_lhs :: LHSType name > , tfe_rhs :: LHsType name } > }}} > > so that the LHS was just a type. Now the renamer can re-jiggle its > fixities in the usual way, and only in the type checker will we need to > decide exactly which type it's an instance of. Easy! > > This might be a good change to make! It's a bit like in ClsInstDecl, you'll > see that the instance cid_poly_ty is just a LHsSigType, i.e. not decomposed > into which class it is. > -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11307> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #12430: TypeFamilyDependencies accepts invalid injectivity annotation
by GHC 16 Oct '18

16 Oct '18

#12430: TypeFamilyDependencies accepts invalid injectivity annotation -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | 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: -------------------------------------+------------------------------------- Consider this code (depends on singletons-2.2): {{{#!hs {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeInType, TypeFamilyDependencies, UndecidableInstances #-} module Bug where import Data.Kind (Type) import Data.Singletons.Prelude (Map, SndSym0) import GHC.TypeLits (Nat) data Payload = A | B newtype NewType a = NewType Int type NatList = [(Nat, Payload)] type StripNatList (natList :: NatList) = Map SndSym0 natList type family Family (natList :: NatList) = (r :: Type) | r -> natList where Family '[] = () Family xs = NewType (StripNatList xs) }}} Why GHC is okay with injectivity annotation for `Family`: `r -> natList`? These two types: {{{#!hs type Foo = Family '[ '(0, 'A), '(1, 'B)] type Bar = Family '[ '(0, 'A), '(0, 'B)] }}} are obviously map to the same type: {{{#!hs *Bug Data.Singletons.Prelude> :kind! Foo Foo :: * = NewType ('A :$$$ '['B]) *Bug Data.Singletons.Prelude> :kind! Bar Bar :: * = NewType ('A :$$$ '['B]) }}} ---- If inline `StripNatList` inside `Family` definition: {{{#!hs type family Family (natList :: NatList) = (r :: Type) | r -> natList where Family '[] = () Family xs = NewType (Map SndSym0 xs) }}} or change `StripNatList` definition to type family: {{{#!hs type family StripNatList (natList :: NatList) where StripNatList '[] = '[] StripNatList ('(n, x) ': xs) = x ': StripNatList xs }}} compilation expectedly fails with `Type family equation violates injectivity annotation.` ---- Moreover, if I remove `NewType` from `Family` and change result kind: {{{#!hs type family Family (natList :: NatList) = (r :: [Payload]) | r -> natList where Family xs = StripNatList xs }}} it fails with correct error regardless of `StripNatList` definition. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12430> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #12005: Constraint instances not shown in `:info`
by GHC 14 Oct '18

14 Oct '18

#12005: Constraint instances not shown in `:info` -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.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: -------------------------------------+------------------------------------- {{{ $ ghci -ignore-dot-ghci -XKindSignatures -XRank2Types -XConstraintKinds -XAllowAmbiguousTypes -XInstanceSigs GHCi, version 8.1.20160428: http://www.haskell.org/ghc/ :? for help Prelude> import Data.Kind Prelude Data.Kind> class Defer (p :: Constraint) where defer :: (p => r) -> r Prelude Data.Kind> instance Defer () where defer :: r -> r; defer = id Prelude Data.Kind> :i Defer class Defer (p :: Constraint) where defer :: (p => r) -> r {-# MINIMAL defer #-} -- Defined at <interactive>:2:1 }}} Same happens with the [https://github.com/ekmett/constraints/blob/master/src/Data/Constraint/Defer… Data.Constraint.Deferrable] which defines: {{{#!hs instance (Typeable a, Typeable b) => Deferrable (a ~ b) instance (Deferrable a, Deferrable b) => Deferrable (a, b) instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) }}} but no instances are shown: {{{ ghci> import Data.Constraint.Deferrable ghci> :i Deferrable class Deferrable (p :: Constraint) where deferEither :: proxy p -> (p => r) -> Either String r {-# MINIMAL deferEither #-} -- Defined in ‘Data.Constraint.Deferrable’ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12005> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #8763: forM_ [1..N] does not get fused (10 times slower than go function)
by GHC 13 Oct '18

13 Oct '18

#8763: forM_ [1..N] does not get fused (10 times slower than go function) ------------------------------+-------------------------------------------- Reporter: nh2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Runtime performance bug Unknown/Multiple | Test Case: Difficulty: Unknown | Blocking: Blocked By: | Related Tickets: | ------------------------------+-------------------------------------------- Apparently idiomatic code like {{{forM_ [1.._N]}}} does not get fused away. This can give serious performance problems when unnoticed. {{{ -- Slow: forM_ [0.._N-1] $ \i -> do ... -- Around 10 times faster: loop _N $ \i -> do ... {-# INLINE loop #-} loop :: (Monad m) => Int -> (Int -> m ()) -> m () loop bex f = go 0 where go !n | n == bex = return () | otherwise = f n >> go (n+1) }}} Full code example: https://gist.github.com/nh2/8905997 - the relevant alternatives are commented. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8763> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 86

[GHC] #11368: Pattern synonym name is mangled when patterns are non-exhaustive
by GHC 10 Oct '18

10 Oct '18

#11368: Pattern synonym name is mangled when patterns are non-exhaustive ---------------------------------------+--------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.1 Keywords: PatternSynonyms | Operating System: Linux Architecture: x86 | Type of failure: Other Test Case: | Blocked By: Blocking: | Related Tickets: #11367 Differential Rev(s): | Wiki Page: ---------------------------------------+--------------------------- {{{ pattern A n <- ... where A 0 = ... }}} When a pattern synonym is non-exhaustive its name is mangled: {{{ >>> A 3 "*** Exception: /tmp/tmp.t0h0pMgwWb.hs:(4,1)-(5,14): Non-exhaustive patterns in function $bA }}} “Non-exhaustive patterns in pattern synonym A” [https://ghc.haskell.org/trac/ghc/ticket/11367?replyto=5#comment:1 Comment] from ticket #11367. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11368> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #10783: Partial type signatures should work with pattern synonym signatures
by GHC 10 Oct '18

10 Oct '18

#10783: Partial type signatures should work with pattern synonym signatures -------------------------------------+------------------------------------- Reporter: mpickering | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE PatternSynonyms #-} pattern MyJust :: _ pattern MyJust a = Just a }}} GHC can correctly infer the type for the pattern without the type signature so (to me) it is unexpected that this inferred type is not reported to me when using partial type signatures. It just seems to not be implemented currently. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10783> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #12469: Memory fence on writeIORef missing on ARM
by GHC 06 Oct '18

06 Oct '18

#12469: Memory fence on writeIORef missing on ARM ------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Keywords: memory model | Operating System: Unknown/Multiple Architecture: arm | Type of failure: None/Unknown Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: ------------------------------------+------------------------------------- The memory model question has been debated now and again. his thread from ten years back (https://mail.haskell.org/pipermail/haskell-prime/2006-April/001237.html) lays out the basic situation with thunk update, writeIORef, and memory fences. But we recently began experimenting with GHC on ARM platforms, and it seems to lack a memory fence that the participants in the cited thread expect it to have. Here's an attempt to construct a program which writes fields of a data structure, and then writes the pointer to that structure to an IORef, without the proper fence inbetween: ```Haskell import Data.IORef import Control.Concurrent data Foo = Foo Int deriving Show {-# NOINLINE mkfoo #-} mkfoo x = Foo x {-# NOINLINE dowrite #-} dowrite r n = writeIORef r $! mkfoo n main = do r <- newIORef (Foo 3) forkIO (dowrite r 4) x <- readIORef r print x ``` Here's the relevant bits of the CMM that results when compiled on an ARM 64 machine: ```C mkfoo_rn1_entry() // [] { [] } {offset c40i: P64[MainCapability+872] = P64[MainCapability+872] + 16; if (P64[MainCapability+872] > I64[MainCapability+880]) goto c40m; else goto c40l; c40m: I64[MainCapability+928] = 16; P64[MainCapability+24] = mkfoo_rn1_closure; call (I64[MainCapability+16])(R1) args: 16, res: 0, upd: 8; c40l: I64[P64[MainCapability+872] - 8] = Foo_con_info; P64[P64[MainCapability+872]] = P64[I64[MainCapability+856]]; P64[MainCapability+24] = P64[MainCapability+872] - 7; I64[MainCapability+856] = I64[MainCapability+856] + 8; call (I64[P64[I64[MainCapability+856]]])(R1) args: 8, res: 0, upd: 8; } } ``` ```C dowrite_entry() // [] { [] } {offset c44j: call a_r3Dy_entry() args: 24, res: 0, upd: 8; } } a_r3Dy_entry() // [R1] { [] } {offset c41D: if (I64[MainCapability+856] - 16 < I64[MainCapability+864]) goto c41H; else goto c41I; c41H: P64[MainCapability+24] = a_r3Dy_closure; call (I64[MainCapability+16])(R1) args: 24, res: 0, upd: 8; c41I: I64[I64[MainCapability+856] - 8] = block_c41B_info; P64[I64[MainCapability+856] - 16] = P64[I64[MainCapability+856] + 8]; I64[MainCapability+856] = I64[MainCapability+856] - 16; call mkfoo_rn1_entry() args: 16, res: 8, upd: 8; } } block_c41B_entry() // [R1] { [] } {offset c41B: _s3Ep::P64 = P64[I64[MainCapability+856] + 8]; I64[I64[MainCapability+856] + 8] = block_c41G_info; _s3Es::P64 = P64[MainCapability+24]; P64[MainCapability+24] = _s3Ep::P64; P64[I64[MainCapability+856] + 16] = _s3Es::P64; I64[MainCapability+856] = I64[MainCapability+856] + 8; if (P64[MainCapability+24] & 7 != 0) goto u41S; else goto c41K; u41S: call block_c41G_entry(R1) args: 0, res: 0, upd: 0; c41K: call (I64[I64[P64[MainCapability+24]]])(R1) args: 8, res: 8, upd: 8; } } block_c41G_entry() // [R1] { [] } {offset c41G: _s3Ev::P64 = P64[P64[MainCapability+24] + 7]; P64[_s3Ev::P64 + 8] = P64[I64[MainCapability+856] + 8]; call "ccall" arg hints: [PtrHint, PtrHint] result hints: [] dirty_MUT_VAR(MainCapability+24, _s3Ev::P64); P64[MainCapability+24] = ()_closure+1; I64[MainCapability+856] = I64[MainCapability+856] + 16; call (I64[P64[I64[MainCapability+856]]])(R1) args: 8, res: 0, upd: 8; } } ``` The fence should happen before the write of the pointer into the IORef. I can't find the fence, and can't find a codepath in the compiler that would insert it (i.e. with MO_WriteBarrier). `dirty_MUT_VAR` is actually too late to perform the fence, but it doesn't either: ```C void dirty_MUT_VAR(StgRegTable *reg, StgClosure *p) { Capability *cap = regTableToCapability(reg); if (p->header.info == &stg_MUT_VAR_CLEAN_info) { p->header.info = &stg_MUT_VAR_DIRTY_info; recordClosureMutated(cap,p); } } ``` (Neither does `recordClosureMutated`.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12469> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 33

[GHC] #8708: Kind annotation in tuple not parsed
by GHC 05 Oct '18

05 Oct '18

#8708: Kind annotation in tuple not parsed -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Parser) | Version: 7.7 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- Consider this: {{{ {-# LANGUAGE KindSignatures #-} foo :: (Int, Int :: *) foo = undefined }}} HEAD reports {{{ /Users/rae/temp/Bug.hs:5:18: parse error on input ‛::’ }}} Changing the line to {{{ foo :: (Int, (Int :: *)) }}} fixes the problem. Note the extra parentheses. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8708> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #11622: Annotating types in type familiy equations without parentheses
by GHC 05 Oct '18

05 Oct '18

#11622: Annotating types in type familiy equations without parentheses -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.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: -------------------------------------+------------------------------------- When annotating types in right-hand side of type family equations parentheses are required: {{{#!hs type family F a where F _ = (Int :: Type) }}} instead of {{{#!hs type family F a where F _ = Int :: Type }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11622> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6