[GHC] #12922: Kind classes compile with PolyKinds
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | 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: -------------------------------------+------------------------------------- I was asking around on #haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds. To study it, I was working with the following small example: {{{ {-# LANGUAGE TypeFamilies, GADTs, TypeOperators, DataKinds, PolyKinds #-} module Main where import Data.Kind (Type) -- Define a Type for the natural numbers, Zero and a successor data Nat = Z | S Nat class Addable k where type (a :: k) + (b :: k) :: k instance Addable Nat where type (Z + a) = a }}} (for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930) Since according to a responder on #haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds. As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Tritlo: @@ -20,0 +20,1 @@ + type (S a) + b = S (a + b) New description: I was asking around on #haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds. To study it, I was working with the following small example: {{{ {-# LANGUAGE TypeFamilies, GADTs, TypeOperators, DataKinds, PolyKinds #-} module Main where import Data.Kind (Type) -- Define a Type for the natural numbers, Zero and a successor data Nat = Z | S Nat class Addable k where type (a :: k) + (b :: k) :: k instance Addable Nat where type (Z + a) = a type (S a) + b = S (a + b) }}} (for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930) Since according to a responder on #haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds. As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Tritlo: @@ -20,1 +20,1 @@ - type (S a) + b = S (a + b) + type (S a) + b = S (a + b) New description: I was asking around on #haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds. To study it, I was working with the following small example: {{{ {-# LANGUAGE TypeFamilies, GADTs, TypeOperators, DataKinds, PolyKinds #-} module Main where import Data.Kind (Type) -- Define a Type for the natural numbers, Zero and a successor data Nat = Z | S Nat class Addable k where type (a :: k) + (b :: k) :: k instance Addable Nat where type (Z + a) = a type (S a) + b = S (a + b) }}} (for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930) Since according to a responder on #haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds. As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): For a simpler example, this compiles in GHC 8.0.1 (but probably shouldn't) without `TypeInType`: {{{#!hs {-# LANGUAGE PolyKinds #-} type KindOf (a :: k) = k }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Tritlo: @@ -7,1 +7,1 @@ - {-# LANGUAGE TypeFamilies, GADTs, TypeOperators, DataKinds, PolyKinds #-} + {-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds #-} @@ -10,3 +10,1 @@ - import Data.Kind (Type) - - -- Define a Type for the natural numbers, Zero and a successor + -- Define a Type for the natural numbers, zero and a successor @@ -21,0 +19,3 @@ + + main :: IO () + main = putStrLn "Shouldn't this need TypeInType?" New description: I was asking around on #haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds. To study it, I was working with the following small example: {{{ {-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds #-} module Main where -- Define a Type for the natural numbers, zero and a successor data Nat = Z | S Nat class Addable k where type (a :: k) + (b :: k) :: k instance Addable Nat where type (Z + a) = a type (S a) + b = S (a + b) main :: IO () main = putStrLn "Shouldn't this need TypeInType?" }}} (for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930) Since according to a responder on #haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds. As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Without thinking too deeply * `TypeInType` should imply `PolyKinds`. * `PolyKinds` should be enough for kind classes, if by "kind classes" you mean polymorphism over types of kind `Constraint`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire Comment: But look at the OP's {{{ class Addable k where type (a :: k) + (b :: k) :: k }}} where the class variable `k` is used as a kind. This indeed should not be allowed unless `TypeInType` is on. I'll put this in my queue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Welcome Tritlo! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: wontfix | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: new => closed * resolution: => wontfix Comment: We no longer distinguish between `TypeInType` and `PolyKinds`, so I'm closing this ticket. See https://github.com/ghc-proposals/ghc- proposals/blob/master/proposals/0020-no-type-in-type.rst and #15195 for more details. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: wontfix | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Hm... I wonder if we should convert the `TypeInType` Trac keyword to `PolyKinds` as well? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12922: Kind classes compile with PolyKinds -------------------------------------+------------------------------------- Reporter: Tritlo | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: wontfix | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): Technically `TypeInType` also covers `DataKinds`. I wouldn't worry about this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12922#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC