January 2018 - ghc-tickets

[GHC] #14164: GHC hangs on type family dependency
by GHC 12 Jul '18

12 Jul '18

#14164: GHC hangs on type family dependency -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 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: -------------------------------------+------------------------------------- {{{#!hs {-# Language TypeOperators, DataKinds, PolyKinds, KindSignatures, TypeInType, GADTs, TypeFamilyDependencies #-} import Data.Kind type Cat a = a -> a -> Type data SubList :: Cat [a] where SubNil :: SubList '[] '[] Keep :: SubList xs ys -> SubList (x:xs) (x:ys) Drop :: SubList xs ys -> SubList xs (x:ys) type family UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res -> pf ys' xs where UpdateWith '[] '[] SubNil = '[] UpdateWith (y:ys) '[] SubNil = y:ys -- UpdateWith '[] (_:_) (Keep _) = '[] UpdateWith (y:ys) (_:xs) (Keep rest) = y:UpdateWith ys xs rest -- UpdateWith ys (x:xs) (Drop rest) = x:UpdateWith ys xs rest }}} seems to loop forever on the "`Renamer/typechecker`" {{{ $ ghci -ignore-dot-ghci -v /tmp/u.hs GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help Glasgow Haskell Compiler, Version 8.3.20170605, stage 2 booted by GHC version 8.0.2 [...] *** Parser [Main]: !!! Parser [Main]: finished in 1.31 milliseconds, allocated 0.651 megabytes *** Renamer/typechecker [Main]: [hangs] }}} while {{{#!hs type family UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res -> pf ys' xs where UpdateWith '[] '[] SubNil = '[] UpdateWith (y:ys) '[] SubNil = y:ys UpdateWith '[] (_:_) (Keep _) = '[] }}} immediately gives {{{ $ ghc -ignore-dot-ghci /tmp/u.hs [1 of 1] Compiling Main ( /tmp/u.hs, /tmp/u.o ) /tmp/u.hs:14:3: error: • Type family equations violate injectivity annotation: UpdateWith '[] '[] 'SubNil = '[] -- Defined at /tmp/u.hs:14:3 forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1). UpdateWith '[] (_2 : _1) ('Keep _3) = '[] -- Defined at /tmp/u.hs:16:3 • In the equations for closed type family ‘UpdateWith’ In the type family declaration for ‘UpdateWith’ | 14 | UpdateWith '[] '[] SubNil = '[] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ /tmp/u.hs:16:3: error: • Type family equation violates injectivity annotation. Type and kind variables ‘_2’, ‘_1’, ‘xs’, ‘_3’ cannot be inferred from the right-hand side. Use -fprint-explicit-kinds to see the kind arguments In the type family equation: forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1). UpdateWith '[] (_2 : _1) ('Keep _3) = '[] -- Defined at /tmp/u.hs:16:3 • In the equations for closed type family ‘UpdateWith’ In the type family declaration for ‘UpdateWith’ | 16 | UpdateWith '[] (_:_) (Keep _) = '[] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14164> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 16

[GHC] #14174: GHC panic with TypeInType and type family
by GHC 10 Jul '18

10 Jul '18

#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: TypeInType | 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: -------------------------------------+------------------------------------- This rather simple type family, {{{#!hs {-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-} module GenWhoops where import GHC.Generics type family GenComp k (x :: k) (y :: k) :: Ordering where GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y }}} produces the following panic: {{{ ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170828 for x86_64-unknown-linux): piResultTy k_a1LK[tau:1] p_a1Lz[sk:1] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type }}} This happens with both GHC 8.2.1 and something very close to HEAD. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #12050: Allow haddock comments on non-record types
by GHC 10 Jul '18

10 Jul '18

#12050: Allow haddock comments on non-record types -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 (Parser) | 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: -------------------------------------+------------------------------------- There are a variety of cases I have found myself wanting to place haddock documentation on fields of non-record data types rather often in the past. The syntax for this might look like, {{{#!hs data Foo = Foo -- ^ A foo Int -- ^ how big is the foo? String -- ^ the name of the foo }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12050> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #8822: Allow -- ^ Haddock syntax on record constructors
by GHC 10 Jul '18

10 Jul '18

#8822: Allow -- ^ Haddock syntax on record constructors -------------------------------------+------------------------------------- Reporter: Fuuzetsu | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Parser) | Version: 7.9 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- Original ticket is on Haddock Trac [http://trac.haskell.org/haddock/ticket/144 here] which I'm opening here as it requires lexer/parser changes. The idea is that given something like {{{ -- | A tree with labeled internal nodes data Tree = Empty -- ^ Leaf | Branch -- ^ Internal node { label :: a -- ^ Node label , subtrees :: [Tree] -- ^ List of subtrees } }}} we'd like it to parse as the user would expect instead of failing. We're currently forced to do something like {{{ -- | A tree with labeled internal nodes data Tree = Empty -- ^ Leaf | -- | Internal node Branch { label :: a -- ^ Node label , subtrees :: [Tree] -- ^ List of subtrees } }}} which is quite ugly. I can't think of a reason why the first form wouldn't be allowed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8822> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8
by GHC 10 Jul '18

10 Jul '18

#11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8 -------------------------------------+------------------------------------- Reporter: cactus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | 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: -------------------------------------+------------------------------------- Given the following definitions (just a copy of the relevant bits from sized-types 0.3.5.1, to keep this example self-contained): {{{ -- Copied from sized-types 0.3.5.1 data X0 = X0 data N1 = N1 data X0_ a = X0_ Integer data X1_ a = X1_ Integer type X1 = X1_ X0 type X2 = X0_ (X1_ X0) class Size ix instance Size X0 instance Size a => Size (X1_ a) instance Size a => Size (X0_ a) type family APP0 a type instance APP0 X0 = X0 type instance APP0 N1 = X0_ N1 type instance APP0 (X1_ a) = X0_ (X1_ a) type instance APP0 (X0_ a) = X0_ (X0_ a) type family APP1 a type instance APP1 X0 = X1_ X0 type instance APP1 N1 = N1 type instance APP1 (X1_ a) = X1_ (X1_ a) type instance APP1 (X0_ a) = X1_ (X0_ a) type family SUCC a type instance SUCC X0 = X1_ X0 type instance SUCC N1 = X0 type instance SUCC (X1_ a) = APP0 (SUCC a) type instance SUCC (X0_ a) = APP1 a type family ADD a b type instance ADD a X0 = a type instance ADD X0 a = a type instance ADD X0 N1 = N1 type instance ADD N1 N1 = APP0 N1 type instance ADD N1 (X1_ b) = APP0 b type instance ADD N1 (X0_ b) = APP1 (ADD N1 b) type instance ADD (X1_ a) N1 = APP0 a type instance ADD (X0_ a) N1 = APP1 (ADD a N1) type instance ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b)) type instance ADD (X1_ a) (X0_ b) = APP1 (ADD a b) type instance ADD (X0_ a) (X1_ b) = APP1 (ADD a b) type instance ADD (X0_ a) (X0_ b) = APP0 (ADD a b) type family NOT a type instance NOT X0 = N1 type instance NOT N1 = X0 type instance NOT (X1_ a) = APP0 (NOT a) type instance NOT (X0_ a) = APP1 (NOT a) type SUB a b = ADD a (SUCC (NOT b)) }}} The following module typechecks with GHC 7.8.3: {{{ data B w = B (&*) :: (Size n, Size n', Size (ADD n' n), n ~ SUB (ADD n' n) n', n' ~ SUB (ADD n' n) n) => [(a, B n)] -> [(b, B n')] -> [((a, b), B (ADD n' n))] mks &* args = undefined foo :: [((), B X1)] foo = [((), B)] bar :: [(((), ()), B X2)] bar = [((), B)] &* foo }}} However, it fails with GHC 7.10.2, with {{{ /tmp/GHCBug.hs:70:7: Couldn't match type ‘ADD X1 n0’ with ‘X0_ (X1_ X0)’ The type variable ‘n0’ is ambiguous Expected type: [(((), ()), B X2)] Actual type: [(((), ()), B (ADD X1 n0))] In the expression: [((), B)] &* foo In an equation for ‘bar’: bar = [((), B)] &* foo /tmp/GHCBug.hs:70:17: Occurs check: cannot construct the infinite type: n0 ~ ADD (ADD X1 n0) N1 The type variable ‘n0’ is ambiguous Expected type: SUB (ADD X1 n0) X1 Actual type: n0 In the expression: [((), B)] &* foo In an equation for ‘bar’: bar = [((), B)] &* foo Failed, modules loaded: none. }}} The workaround/solution is to change the definition of `bar`: {{{ bar :: [(((), ()), B X2)] bar = [((), B :: B X1)] &* foo }}} This second version typechecks with GHC 7.10.2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11070> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #13109: CUSK improvements
by GHC 10 Jul '18

10 Jul '18

#13109: CUSK improvements -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.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: -------------------------------------+------------------------------------- Inspired by looking at `RnTypes.bindLHsTyVarBndr`, and driven by #11592, Richard and I decided to make some improvements to the treatment of CUSKs. Here's a scrappy Skype dump as a memory-jogger; it is a memory-jogger, not a full description. Richard has notes too {{{ Richard Eisenberg: data F (x :: B a) data G (x :: C b) You have written a complete user-suppled kind signature, but the following variable is undetermined: a0 :: A Perhaps add a kind signature. Inferred kinds of user-written variables: b :: B a0 x :: C b SPJ claim: CUSKs should be handled INDIVIDUALLY and in isoloation, just like term-level type signatures SPJ claim: get rid of the "after the ::" side condition for data types (last bullet of HsDecls Note about CUSKs All of this should mean (SPJ claims) no need for dep_vars returns by bindHsQTyVar, bindLHsTyVarBnrds etc ToDo: clarify comments etc in bindLHStyVarBndr Related to D2914 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13109> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #11282: Injectivity annotation fails in the presence of higher-rank use of constraint family
by GHC 09 Jul '18

09 Jul '18

#11282: Injectivity annotation fails in the presence of higher-rank use of constraint family -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: 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: -------------------------------------+------------------------------------- When I say {{{ {-# LANGUAGE TypeFamilies, RankNTypes #-} module Bug where import GHC.Exts type family F a = r | r -> a type family G a :: Constraint meth :: (G a => F a) -> () meth = undefined }}} I get {{{ Bug.hs:10:9: error: • Could not deduce: F a ~ F a0 from the context: G a0 bound by the type signature for: meth :: G a0 => F a0 at Bug.hs:10:9-26 NB: ‘F’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous • In the ambiguity check for ‘meth’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: meth :: (G a => F a) -> () }}} The presence of `G a` is critical for exhibiting this bug. If I replace `G a` with `Show a` the problem disappears. This one was actually encountered in an attempt to do Useful Work, not just idle typecheckery. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11282> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #12928: Too easy to trigger CUSK condition using TH
by GHC 09 Jul '18

09 Jul '18

#12928: Too easy to trigger CUSK condition using TH -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: feature | Status: new request | Priority: high | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | 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: -------------------------------------+------------------------------------- While trying to make `singletons` class promotion work with kind- polymorphic type variables, I've encountered a problem regarding CUSKs. Consider this class: {{{ $(promoteOnly [d| class Cls a where fff :: Proxy a -> () |]) }}} The generated TH (slightly simplified by hand) looks like this: {{{ type FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm data FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ()) type instance Apply FffSym0 l_alvn = FffSym1 l_alvn class PCls a_alve where type Fff (arg_alvl :: Proxy a_alve) :: () }}} However, it fails to compile with the following error: {{{ cusk.hs:25:1: error: You have written a *complete user-suppled kind signature*, but the following variable is undetermined: k0 :: * Perhaps add a kind signature. Inferred kinds of user-written variables: a1627472612 :: k0 l_alvn :: TyFun (Proxy a1627472612) () }}} As suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write {{{ data FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ()) }}} and it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so. Looking at the module `TcHsType` in the GHC sources, I see that the error is reported by the `kcHsTyVarBndrs` function: {{{ -- If there are any meta-tvs left, the user has -- lied about having a CUSK. Error. ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs ; when (not (null meta_tvs)) $ report_non_cusk_tvs (qkvs ++ tc_tvs) }}} However, I don't see why we can't generalize over `meta_tvs` instead of reporting a failure. I asked on IRC #ghc and ezyang suggested that it should be sound. Below I attach a self-contained example that demonstrates the issue and has no dependencies except `base`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12928> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #14091: When PolyKinds is on, suggested type signatures seem to require TypeInType
by GHC 09 Jul '18

09 Jul '18

#14091: When PolyKinds is on, suggested type signatures seem to require TypeInType -------------------------------------+------------------------------------- Reporter: jberryman | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 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: -------------------------------------+------------------------------------- We compile the following with -Wall {{{ {-# LANGUAGE PolyKinds #-} import Data.Bits import Data.Word data Hash128 a = Hash128 { hashWord128_0 :: !Word64, hashWord128_1 :: !Word64 } deriving (Show, Read, Eq) -- These instances copied from 'FixedPoint-simple': instance FiniteBits (Hash128 a) where finiteBitSize ~(Hash128 a b) = finiteBitSize a + finiteBitSize b instance Bits (Hash128 a) where popCount (Hash128 h l) = popCount h + popCount l bit i | i >= 64 = Hash128 (bit $ i - 64) 0 | otherwise = Hash128 0 (bit i) complement = pointwise complement (.&.) = pointwise2 (.&.) (.|.) = pointwise2 (.|.) xor = pointwise2 xor setBit (Hash128 h l) i | i >= 64 = Hash128 (setBit h (i - 64)) l | otherwise = Hash128 h (setBit l i) shiftL (Hash128 h l) i | i > finiteBitSize l = shiftL (Hash128 l 0) (i - finiteBitSize l) | otherwise = Hash128 ((h `shiftL` i) .|. (l `shiftR` (finiteBitSize l - i))) (l `shiftL` i) shiftR (Hash128 h l) i | i > finiteBitSize h = shiftR (Hash128 0 h) (i - finiteBitSize h) | otherwise = Hash128 (h `shiftR` i) ((l `shiftR` i) .|. h `shiftL` (finiteBitSize h - i)) isSigned _ = False testBit (Hash128 h l) i | i >= finiteBitSize l = testBit h (i - finiteBitSize l) | otherwise = testBit l i rotateL w i = shiftL w i .|. shiftR w (128 - i) rotateR w i = shiftR w i .|. shiftL w (128 - i) bitSize _ = 128 bitSizeMaybe _ = Just 128 pointwise op (Hash128 a b) = Hash128 (op a) (op b) pointwise2 op (Hash128 a b) (Hash128 c d) = Hash128 (op a c) (op b d) }}} get a warning like: {{{ Top-level binding with no type signature: pointwise2 :: forall k1 k2 k3 (a1 :: k2) (a2 :: k1) (a3 :: k3). (Word64 -> Word64 -> Word64) -> Hash128 a1 -> Hash128 a2 -> Hash128 a3 }}} but that's not a valid signature. Pasting it in causes GHC to suggest RankNTypes with an error, and then to suggest TypeInType, at which point it compiles. I want to just be able to paste in the signature from the warning. Related to #6065 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14091> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[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