[GHC] #14238: `:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1
GHC
ghc-devs at haskell.org
Fri Sep 15 14:17:18 UTC 2017
#14238: `:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.2.1
(Type checker) |
Keywords: TypeInType | Operating System: Unknown/Multiple
Architecture: | Type of failure: Incorrect result
Unknown/Multiple | at runtime
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
Load this program into GHCi on 8.2.1 or later:
{{{#!hs
{-# 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
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14238>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list