Opened 5 years ago

Last modified 4 years ago

#10179 new bug

Kinds missing from types in ghci

Reported by: br1 Owned by:
Priority: normal Milestone:
Component: GHCi Version: 7.10.1-rc2
Keywords: Cc: hvr
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #8809,#10073,#10179 Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

{-# 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

Change History (4)

comment:1 Changed 5 years ago by simonpj

Description: modified (diff)

comment:2 Changed 5 years ago 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?

comment:3 Changed 5 years ago 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 ks 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.

comment:4 Changed 4 years ago by thomie

Note: See TracTickets for help on using tickets.