[GHC] #10179: Kinds missing from types in ghci
#10179: Kinds missing from types in ghci -------------------------------------+------------------------------------- Reporter: br1 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.10.1-rc2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} data family F (a:: k) foo :: F (m :: [()]) -> a foo = undefined bar :: F (m :: [[()]]) -> a bar = undefined according to GHCi, both foo and bar have type F m -> a but [foo, bar] fails -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10179 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10179: Kinds missing from types in ghci -------------------------------------+------------------------------------- Reporter: br1 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-}
data family F (a:: k)
foo :: F (m :: [()]) -> a foo = undefined bar :: F (m :: [[()]]) -> a bar = undefined
according to GHCi, both foo and bar have type F m -> a but [foo, bar] fails
New description: {{{ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} data family F (a:: k) foo :: F (m :: [()]) -> a foo = undefined bar :: F (m :: [[()]]) -> a bar = undefined }}} according to GHCi, both `foo` and `bar` have type `F m -> a` but `[foo, bar]` fails -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10179#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10179: Kinds missing from types in ghci -------------------------------------+------------------------------------- Reporter: br1 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Good point. The question is this: '''when pretty-printing a type, when and how should we display kind annotations?'''. Currenty in GHCi we by- default suppress foralls and kind annotations. (NB: by the time we get to "pretty print this type" we've lost touch with the original source-language type signature, and in any case the same rules should apply for inferred types.) For example, this is what happens currently (without `-fprint-explicit- foralls` and `-fprint-explicit-kinds`): {{{ Type Display ------------------------------------------------------------------------------- 1. f :: forall (a::*). a->a f :: a->a 2. f :: forall (m::*->*) (a::*). m a -> a f :: m a -> a 3. f :: forall (k::BOX) (m::k->*) (a::k). m a -> m a f :: m a -> m a ??? 4. f :: forall (m::*->*) (a::*). m a -> m a f :: m a -> m a ??? }}} Note that * In (2) the kinds are forced by the rest of the type `m a -> a` * In (3), assuming `-XPolyKinds` the type on the left is the most kind- polymorphic type compatible with the type on the right. * In (4) the kind polymoprhism has been squashed out, as it has in the ticket description. The trouble is that (3) and (4) are displayed the same, even though they are different. It's hard to even say exactly what we want here! Perhaps something like "print the kind-attributed foralls explicitly, unless the kinds are implied by the most-kind-polymorphic reading of the signature"; but that's quite complicated. Ideas? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10179#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10179: Kinds missing from types in ghci -------------------------------------+------------------------------------- Reporter: br1 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: GHCi | Version: 7.10.1-rc2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): I think the problem here is that GHC/the Haskell community, in general, is quite ambivalent about kind-polymorphism. My take on it all is that the power users want it. At the same time, we're afraid that it will scare people, and so we're a little embarrassed of those `k`s showing up to unsuspecting folks without deep experience with type theory. So, we hide the kinds behind `-fprint-explicit-kinds`. I don't think we'll resolve this tension anytime soon, as it's there for a good reason: we want both power and comprehensibility. But it's hard to have both, of course. So, here's a solution: do (broadly) what Idris does. (I don't have Idris to hand, so don't take the analogy too literally.) When a type prints out, suppress kinds. BUT, have some interactive way of requesting more information, say by clicking on the type. I know this solution will take a lot of work, but I think that work will be very worthwhile down the road. See, for example, #10073. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10179#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC