Opened 15 months ago

Closed 8 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:

Description

Load this program into GHCi on 8.2.1 or later:

{-# LANGUAGE GADTs #-}
{-# 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: http://www.haskell.org/ghc/  :? 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: http://www.haskell.org/ghc/  :? 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 15 months 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 15 months 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 9 months ago by RyanGlScott

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

comment:4 Changed 8 months ago by Ryan Scott <ryan.gl.scott@…>

In 718a0181/ghc:

Fix #14238 by always pretty-printing visible tyvars

Summary:
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: https://phabricator.haskell.org/D4564

comment:5 Changed 8 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.