Opened 2 years ago

Closed 18 months ago

#14238 closed bug (fixed)

`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect result at runtime Test Case: dependent/ghci/T14238
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4564
Wiki Page:


Load this program into GHCi on 8.2.1 or later:

{-# LANGUAGE TypeInType #-}

import Data.Kind

data Foo (k :: Type) :: k -> Type where
  MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)

And ask it what the kind of Foo is:

GHCi, version 8.2.1:  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :k Foo
Foo :: k -> *

This is just plain wrong: the actual kind of Foo should be forall k -> k -> *. Normally, one can omit foralls from a kind signature, but this is a special case where we're using a visible forall. In other words, forall k -> k -> * is not the same as k -> *, as the former takes two arguments, whereas the latter takes one.

A workaround is to force GHCi to come to its senses by explicitly enabling -fprint-explicit-foralls:

λ> :set -fprint-explicit-foralls 
λ> :k Foo
Foo :: forall k -> k -> *

This is actually a regression since GHC 8.0.2, since GHCi did the right thing by default then:

GHCi, version 8.0.2:  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )
Ok, modules loaded: Main.
λ> :k Foo
Foo :: forall k -> k -> Type

Change History (5)

comment:1 Changed 2 years ago by simonpj

I agree!

For terms we have a difference between :info (which takes a name) and :type (which takes an expression, and may involve instantiating and re-generalising).

comment:2 Changed 2 years ago by goldfire

Agreed as well. The ticket has TypeInType on it already, and so I'll get to it in due course, unless someone grabs it sooner.

comment:3 Changed 18 months ago by RyanGlScott

Differential Rev(s): Phab:D4564
Status: newpatch

comment:4 Changed 18 months ago by Ryan Scott <…>

In 718a0181/ghc:

Fix #14238 by always pretty-printing visible tyvars

Before, GHC would never print visible tyvars in the absence
of `-fprint-explicit-foralls`, which led to `:kind` displaying
incorrect kinds in GHCi. The fix is simple—simply check beforehand
if any of the type variable binders are required when deciding when
to pretty-print them.

Test Plan: make test TEST=T14238

Reviewers: simonpj, goldfire, bgamari

Subscribers: thomie, carter

GHC Trac Issues: #14238

Differential Revision:

comment:5 Changed 18 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: patchclosed
Test Case: dependent/ghci/T14238
Note: See TracTickets for help on using tickets.