December 2018 - ghc-tickets

[GHC] #15602: PAP invariant of pointer tagging does not hold
by GHC 16 Jan '19

16 Jan '19

#15602: PAP invariant of pointer tagging does not hold -------------------------------------+------------------------------------- Reporter: osa1 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #15508, #13767 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The PAP invariant of pointer tagging says > the PAP entry code jumps to the function's entry code, so it must have a tagged pointer to the function closure in R1. We therefore assume that a PAP always contains a tagged pointer to the function closure. (from https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/HaskellExecution/Point…) As discovered while debugging #15508, this currently does not hold. I tried to fix this in one PAP allocation site in Phab:D5051 but it somehow broke another test. We should review all PAP allocation sites and make sure the invariant holds, and then fix any bugs that this fix reveals. Relevant commits: - 6015a94f9108a502150565577b66c23650796639: Implements pointer tagging - f9c6d53fe997f1c560cda6f346f4b201711df37c: Fixes a PAP allocation site (#13767) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15602> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #12045: Visible kind application
by GHC 16 Jan '19

16 Jan '19

#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple TypeApplications TypeInType | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I've wanted this for a while {{{ ghci> :kind (:~:) (:~:) :: k -> k -> Type }}} {{{ ghci> :kind (:~:) @(Type -> Type) (:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type ghci> :kind (:~:) @(Type -> Type) [] (:~:) @(Type -> Type) [] :: (Type -> Type) -> Type ghci> :kind (:~:) @(Type -> Type) [] Maybe (:~:) @(Type -> Type) [] Maybe :: Type }}} Working like {{{ ghci> type Same k (a::k) (b::k) = a :~: b ghci> :kind Same Same :: forall k -> k -> k -> * }}} {{{ ghci> :kind Same (Type -> Type) Same (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> * ghci> :kind Same (Type -> Type) [] Same (Type -> Type) [] :: (Type -> Type) -> * ghci> :kind Same (Type -> Type) [] Maybe Same (Type -> Type) [] Maybe :: * }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12045> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 22

[GHC] #15592: Type families without CUSKs cannot be given visible kind variable binders
by GHC 16 Jan '19

16 Jan '19

#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple TypeApplications, TypeFamilies, | CUSKs | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following program and GHCi session which uses it: {{{ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Foo where import Data.Kind type family T1 (x :: Type) (y :: a) :: Type where {} type family T2 x (y :: a) :: Type where {} }}} {{{ $ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit- foralls GHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Foo ( Foo.hs, interpreted ) Ok, one module loaded. λ> :kind T1 T1 :: forall a. * -> a -> * λ> :kind T2 T2 :: forall {k} {a}. k -> a -> * }}} Note that `T1` quantifies `a` visibly whereas `T2` does not. I find this somewhat surprising, since both `T1` and `T2` explicitly mention `a` in their respective definitions. The only difference between the two is that `T1` has a CUSK while `T2` does not. This isn't of much importance at the moment, but it will be once visible kind application lands, as this will prevent anyone from instantiating the `a` in `T2` using a kind application. It's unclear to me whether this is intended behavior or not. I suppose there might be an unwritten rule that you can't use visible kind application on anything that doesn't have a CUSK, but if this really is the case, we should be upfront about it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 26

[GHC] #15801: "ASSERT failed!" with visible kind applications
by GHC 16 Jan '19

16 Jan '19

#15801: "ASSERT failed!" with visible kind applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Sorry for the workload mnguyen. This gives a very short error (using diff for visible kind application: https://phabricator.haskell.org/D5229) {{{#!hs {-# Language CPP #-} {-# Language QuantifiedConstraints #-} {-# Language TypeApplications #-} {-# Language PolyKinds #-} {-# Language TypeOperators #-} {-# Language DataKinds #-} {-# Language TypeFamilies #-} {-# Language TypeSynonymInstances #-} {-# Language FlexibleInstances #-} {-# Language GADTs #-} {-# Language UndecidableInstances #-} {-# Language MultiParamTypeClasses #-} {-# Language FlexibleContexts #-} import Data.Coerce import Data.Kind type Cat ob = ob -> ob -> Type type Obj = Type class Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b) instance Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b) class (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj instance (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj class Ríki (obj :: Obj) where type (-->) :: obj -> obj -> Type ið :: a --> (a::obj) class OpOpNoOp obj => OpRíki (obj :: Obj) where type (<--) :: obj -> obj -> Type data Op a = Op a type family UnOp op where UnOp ('Op obj) = obj newtype Y :: Cat (Op a) where Y :: (UnOp b --> UnOp a) -> Y a b instance Ríki Type where type (-->) = (->) ið x = x instance OpRíki (Op Type) where type (<--) @(Op Type) = Y @Type }}} {{{ $ ghci -ignore-dot-ghci 577.hs GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 577.hs, interpreted ) *** Exception: ASSERT failed! file compiler/typecheck/TcFlatten.hs, line 1285 > }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15801> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #15795: Core lint error with visible kind patterns
by GHC 16 Jan '19

16 Jan '19

#15795: Core lint error with visible kind patterns -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Finally managed to trigger a core lint error with #12045 {{{#!hs {-# Language RankNTypes #-} {-# Language TypeApplications #-} {-# Language DataKinds #-} {-# Language PolyKinds #-} {-# Language TypeOperators #-} {-# Language GADTs #-} {-# Options_GHC -dcore-lint #-} import Data.Kind type Cat ob = ob -> ob -> Type data (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2) where Prod :: forall ob1 ob2 cat1 cat2 a1 b1 a2 b2 u. cat1 a1 b1 -> cat2 a2 b2 -> (×) @u '(a1, a2) '(b1, b2) }}} log attached from running `ghci -ignore-dot-ghci <file>.hs` -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15795> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #16013: :kind! accepts unsaturated type aliases
by GHC 16 Jan '19

16 Jan '19

#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.4.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: -------------------------------------+------------------------------------- Here's a ghci session: {{{ > :set -XTypeFamilies -XPolyKinds > type family Id (a :: k) > type instance Id a = a > type Foo x = Maybe > :kind! Id Foo Id Foo :: * = Id Foo }}} I think the final `:kind!` query should throw an error instead, complaining that `Foo` hasn't been given enough arguments. (But even if you disagree, and think it should be allowed, `*` is clearly not the right kind!) Using a normal type alias in place of the type family for `Id` also allows the query incorrectly, though it does at least report a sensible kind. Although I think it shouldn't matter, I have checked with `-ignore-dot- ghci` to make sure I haven't accidentally turned LiberalTypeSynonyms on. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #15816: Visible kind applications + data family: `U :: Type' said to be of kind `k0 -> k1` in error message
by GHC 16 Jan '19

16 Jan '19

#15816: Visible kind applications + data family: `U :: Type' said to be of kind `k0 -> k1` in error message -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Using the [https://phabricator.haskell.org/D5229 visible kind applications (D5229)] (#12045) patch. GHC erroneously calls `U :: Type` a "function" of kind `k0 -> k1` if I understand this right, {{{ $ ghci GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help Prelude> :set prompt "> " > import Data.Kind (Type) > > :set -XTypeFamilies > :set -XTypeApplications > > data family U :: Type > data instance U @Int <interactive>:7:1: error: • Cannot apply function of kind ‘k0 -> k1’ to visible kind argument ‘Int’ • In the data instance declaration for ‘U’ > }}} I expect something like "Cannot apply type `U` to visible kind argument `Int`" or {{{ > data instance U Int = MkU <interactive>:7:1: error: • Expected kind ‘* -> *’, but ‘U’ has kind ‘*’ • In the data instance declaration for ‘U’ > }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15816> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #15362: Template Haskell ignores bad type family definitions
by GHC 16 Jan '19

16 Jan '19

#15362: Template Haskell ignores bad type family definitions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Template | Version: 8.4.3 Haskell | 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 garbage is accepted: {{{#!hs data Nat = Zero | Succ Nat $( [d| type family a + b where Maybe Zero b = b Succ a + b = Succ (a + b) |] ) }}} Note the `Maybe` photo-bombing in the first equation. The problem is that TH uses the symbol declared in the family head for all the equations, ignoring what's actually there. This is sad. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15362> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #15788: Core Lint error, from visible kind applications
by GHC 16 Jan '19

16 Jan '19

#15788: Core Lint error, from visible kind applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: #12045 | 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 RankNTypes #-} {-# Language GADTs #-} {-# Language TypeApplications #-} {-# Language PolyKinds #-} {-# Options_GHC -dcore-lint #-} import Data.Kind data A :: forall k. Type where MkA :: A @k }}} this cute bug crashes under the [https://phabricator.haskell.org/D5229 visible kind application] diff, produces: {{{ $ ghci -ignore-dot-ghci 545_bug.hs GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 545_bug.hs, interpreted ) *** Core Lint errors : in result of Tidy Core *** <no location info>: warning: In the type ‘forall (k :: k_a1xN[sk:1]) k. A’ @ k_a1xN[sk:1] is out of scope *** Offending Program *** $WMkA [InlPrag=INLINE[2]] :: forall (k :: k_a1xN[sk:1]) k. A [GblId[DataConWrapper], Caf=NoCafRefs, Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True) Tmpl= \ (@ (k_a1y5 :: k_a1xN[sk:1])) (@ k_X1xP) -> MkA @ k_X1xP @ k_a1y5}] $WMkA = \ (@ (k_a1y5 :: k_a1xN[sk:1])) (@ k_X1xP) -> MkA @ k_X1xP @ k_a1y5 $trModule1_r1zb :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule1_r1zb = "main"# $trModule2_r1zu :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule2_r1zu = TrNameS $trModule1_r1zb $trModule3_r1zv :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule3_r1zv = "Main"# $trModule4_r1zw :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule4_r1zw = TrNameS $trModule3_r1zv $trModule :: Module [GblId, Caf=NoCafRefs, Unf=OtherCon []] $trModule = Module $trModule2_r1zu $trModule4_r1zw $krep_r1zx :: KindRep [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep_r1zx = KindRepVar 1# $krep1_r1zy :: KindRep [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep1_r1zy = KindRepVar 0# $tcA1_r1zz :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tcA1_r1zz = "A"# $tcA2_r1zA :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tcA2_r1zA = TrNameS $tcA1_r1zz $tcA :: TyCon [GblId, Unf=OtherCon []] $tcA = TyCon 16201120719427956884## 13080046616073797921## $trModule $tcA2_r1zA 2# krep$* $krep2_r1zB :: [KindRep] [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep2_r1zB = : @ KindRep $krep1_r1zy ([] @ KindRep) $krep3_r1zC :: [KindRep] [GblId, Caf=NoCafRefs, Unf=OtherCon []] $krep3_r1zC = : @ KindRep $krep_r1zx $krep2_r1zB $krep4_r1zD :: KindRep [GblId, Unf=OtherCon []] $krep4_r1zD = KindRepTyConApp $tcA $krep3_r1zC $tc'MkA1_r1zE :: Addr# [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tc'MkA1_r1zE = "'MkA"# $tc'MkA2_r1zF :: TrName [GblId, Caf=NoCafRefs, Unf=OtherCon []] $tc'MkA2_r1zF = TrNameS $tc'MkA1_r1zE $tc'MkA :: TyCon [GblId, Unf=OtherCon []] $tc'MkA = TyCon 1695572187443655535## 16213897990811765752## $trModule $tc'MkA2_r1zF 2# $krep4_r1zD *** End of Offense *** <no location info>: error: Compilation had errors *** Exception: ExitFailure 1 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15788> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #15793: Type family doesn't reduce with visible kind application
by GHC 16 Jan '19

16 Jan '19

#15793: Type family doesn't reduce with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- If we un-comment `f2` {{{#!hs {-# Language RankNTypes #-} {-# Language TypeFamilies #-} {-# Language TypeApplications #-} {-# Language PolyKinds #-} import Data.Kind type family F1 (a :: Type) :: Type where F1 a = Maybe a f1 :: F1 a f1 = Nothing type family F2 :: forall (a :: Type). Type where F2 @a = Maybe a -- f2 :: F2 @a -- f2 = Nothing }}} this program fails with {{{ • Couldn't match kind ‘forall a1. *’ with ‘* -> *’ When matching types F2 :: forall a. * Maybe :: * -> * Expected type: F2 Actual type: Maybe a • In the expression: Nothing In an equation for ‘f2’: f2 = Nothing | 20 | f2 = Nothing | ^^^^^^^ Failed, no modules loaded. }}} It also succeeds replacing `Nothing` with `undefined` {{{#!hs f2 :: F2 @a f2 = undefined }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6