[GHC] #15806: Impredicativity behavior in `:k` command in GHCi

25 Oct 2018

      #15806: Impredicativity behavior in `:k` command in GHCi
-------------------------------------+-------------------------------------
           Reporter:  ningning       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #14859
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 In GHCi, the following command works:

 {{{#!hs
 Prelude> :set -XRankNTypes
 Prelude> :k (Maybe (forall a. a -> a))
 (Maybe (forall a. a -> a)) :: *
 }}}

 Note here the type argument of `Maybe` is a polymorphic type.

 However the following would be (correctly) rejected:

 {{{#!hs
 Prelude> let f :: (Maybe (forall a. a -> a)) -> Int; f _ = 1

 <interactive>:4:10: error:
     • Illegal polymorphic type: forall a. a -> a
       GHC doesn't yet support impredicative polymorphism
     • In the type signature: f :: (Maybe (forall a. a -> a)) -> Int
 }}}

 Question: why does `:k` behave differently and is it what is expected?

 I think if we have #14859 those are both acceptable though?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15806
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler