[GHC] #15806: Impredicativity behavior in `:k` command in GHCi
GHC
ghc-devs at haskell.org
Thu Oct 25 13:19:07 UTC 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
More information about the ghc-tickets
mailing list