`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1
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 forall
s 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
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |