[GHC] #11252: :kind command hides the explicit kind

#11252: :kind command hides the explicit kind ----------------------------------------+-------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.11 Keywords: TypeInType | Operating System: Linux Architecture: Unknown/Multiple | Type of failure: Other Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: ----------------------------------------+-------------------------- {{{#!hs -- /tmp/test.hs {-# LANGUAGE TypeInType #-} data Proxy1 k (a :: k) = P1 data Proxy2 (a :: k) = P2 }}} if I load the following into ghci (head) the `:kind` command gives the same result {{{#!haskell % ghci -ignore-dot-ghci /tmp/test.hs GHCi, version 7.11.20151216: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( test.hs, interpreted ) Ok, modules loaded: Main. *Main> :kind Proxy1 :kind Proxy1 Proxy1 :: k -> * *Main> :kind Proxy2 :kind Proxy2 Proxy2 :: k -> * }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11252: :kind command hides the explicit kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.11 Resolution: | Keywords: TypeInType Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
{{{#!hs -- /tmp/test.hs {-# LANGUAGE TypeInType #-}
data Proxy1 k (a :: k) = P1 data Proxy2 (a :: k) = P2 }}}
if I load the following into ghci (head) the `:kind` command gives the same result
{{{#!haskell % ghci -ignore-dot-ghci /tmp/test.hs GHCi, version 7.11.20151216: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( test.hs, interpreted ) Ok, modules loaded: Main. *Main> :kind Proxy1 :kind Proxy1 Proxy1 :: k -> * *Main> :kind Proxy2 :kind Proxy2 Proxy2 :: k -> * }}}
New description: {{{#!hs -- /tmp/test.hs {-# LANGUAGE TypeInType #-} data Proxy1 k (a :: k) = P1 data Proxy2 (a :: k) = P2 }}} if I load the following into ghci (head) the `:kind` command gives the same result {{{#!haskell % ghci -ignore-dot-ghci /tmp/test.hs GHCi, version 7.11.20151216: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( test.hs, interpreted ) Ok, modules loaded: Main. *Main> :kind Proxy1 :kind Proxy1 Proxy1 :: k -> * *Main> :kind Proxy2 :kind Proxy2 Proxy2 :: k -> * }}} edit: I asked on #ghc, was told this was undesirable -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11252: :kind command hides the explicit kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.11 Resolution: | Keywords: TypeInType Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
{{{#!hs -- /tmp/test.hs {-# LANGUAGE TypeInType #-}
data Proxy1 k (a :: k) = P1 data Proxy2 (a :: k) = P2 }}}
if I load the following into ghci (head) the `:kind` command gives the same result
{{{#!haskell % ghci -ignore-dot-ghci /tmp/test.hs GHCi, version 7.11.20151216: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( test.hs, interpreted ) Ok, modules loaded: Main. *Main> :kind Proxy1 :kind Proxy1 Proxy1 :: k -> * *Main> :kind Proxy2 :kind Proxy2 Proxy2 :: k -> * }}}
edit: I asked on #ghc, was told this was undesirable
New description: {{{#!hs -- /tmp/test.hs {-# LANGUAGE TypeInType #-} data Proxy1 k (a :: k) = P1 data Proxy2 (a :: k) = P2 }}} if I load the following into ghci (head) the `:kind` command gives the same result {{{#!haskell % ghci -ignore-dot-ghci /tmp/test.hs GHCi, version 7.11.20151216: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( test.hs, interpreted ) Ok, modules loaded: Main. *Main> :kind Proxy1 Proxy1 :: k -> * *Main> :kind Proxy2 Proxy2 :: k -> * }}} edit: I asked on #ghc, was told this was undesirable -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11252: :kind command hides the explicit kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.11 Resolution: | Keywords: TypeInType Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Example from [https://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds- extended.pdf System FC with Explicit Kind Equality (Extended Version)]: {{{#!hs data Kind = Star | Arr Kind Kind data Ty :: Kind -> * where TInt :: Ty Star ... data TypeRep (k :: Kind) (t :: Ty k) where TyInt :: TyRep Star TInt ... }}} gives {{{#!hs
:kind TyRep TyRep :: Ty k -> * }}}
making the user think they should provide a `Ty k` {{{#!hs
:kind TyRep TInt <error> }}}
when they should really provide a `Kind` and ''then'' some `Ty k`: {{{#!hs
:kind TyRep Star TyRep Star :: Ty 'Star -> * :kind TyRep Star TInt TyRep Star TInt :: * }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11252: :kind command hides the explicit kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: feature request | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.11 Resolution: | Keywords: TypeInType Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire Comment: Another bug for me. Will fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11252: :kind command hides the explicit kind
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: goldfire
Type: feature request | Status: new
Priority: normal | Milestone:
Component: GHCi | Version: 7.11
Resolution: | Keywords: TypeInType
Operating System: Linux | Architecture:
| Unknown/Multiple
Type of failure: Other | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#11252: :kind command hides the explicit kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: feature request | Status: merge Priority: normal | Milestone: 8.0.1 Component: GHCi | Version: 7.11 Resolution: | Keywords: TypeInType Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * milestone: => 8.0.1 Comment: It's just the test case that I added. But that should be merged. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11252: :kind command hides the explicit kind -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: feature request | Status: closed Priority: normal | Milestone: 8.0.1 Component: GHCi | Version: 7.11 Resolution: fixed | Keywords: TypeInType Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: This was merged to `ghc-8.0` in b41586be7ba0659216c74ef8a58a0aa4d2cc2195. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC