Opened 9 months ago

Closed 2 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 9 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 9 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 3 months ago by RyanGlScott

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

comment:4 Changed 2 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 2 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.