[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