[GHC] #11963: GHC introduces kind equality without TypeInType
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1-rc2 (Type checker) | 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: -------------------------------------+------------------------------------- The following program is accepted by GHC 8.0 rc2 {{{ {-# LANGUAGE GADTs, PolyKinds, RankNTypes #-} data Typ k t where Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t }}} This probably shouldn't be accepted, because this is a circuitous way of saying: {{{ {-# LANGUAGE TypeInType #-} data Typ k (t :: k) = Typ }}} which does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`? Printing with explicit kinds makes it clear why the obvious check didn't fire: {{{ ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( B.hs, interpreted ) Ok, modules loaded: Main. *Main> :info Typ type role Typ nominal nominal nominal data Typ k k1 (t :: k) where Typ :: forall k (t :: k). (forall (a :: k -> *). a t -> a t) -> Typ k k t -- Defined at B.hs:2:1 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1-rc2 checker) | 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 goldfire): * keywords: => TypeInType Comment: As it says in the user's guide, identifying the necessity for `-XTypeInType` is done on a best-effort basis. That said, I'm surprised this one is missed, because `k` is clearly used as both a kind and a type in the type of the data constructor. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1-rc2 checker) | 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): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1-rc2 checker) | 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 johnleo): * owner: goldfire => johnleo -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11963: GHC introduces kind equality without TypeInType
-------------------------------------+-------------------------------------
Reporter: ezyang | Owner: johnleo
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.1-rc2
checker) |
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: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: johnleo Type: bug | Status: merge Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T11963 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => typecheck/should_fail/T11963 * status: new => merge * milestone: => 8.2.2 Comment: This seems easy enough to merge, but it's far from critical. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: johnleo Type: bug | Status: closed Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T11963 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.2` with 18dee8912f6afdcf13073d3d95d85513c14180e3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: johnleo Type: bug | Status: closed Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T11963 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Reverted from `ghc-8.2` in 5e2d3e6d06a051dd30c0ce1919cd2d3d0ece087b as it causes a few programs from Hackage to be rejected, which we'd like to avoid in a point release. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11963: GHC introduces kind equality without TypeInType -------------------------------------+------------------------------------- Reporter: ezyang | Owner: johnleo Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T11963 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.2 => 8.4.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11963#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC