`: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 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
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 |