New implementation for `ImpredicativeTypes`

Simon Peyton Jones simonpj at
Fri Sep 6 07:33:07 UTC 2019

I’m confused.   Char does not have the type (forall a. Show a =>a), so our example is iill-typed in System F, never mind about type inference.  Perhaps there’s a typo?   I think you may have ment
               exists a. Show a => a
which doesn’t exist in Haskell.  You can write existentials with a data type

data Showable where
   S :: forall a. Show a => a -> Showable

               map show [S 1, S ‘a’, S “b”]
works fine today (without our new stuff), provided you say

               instance Show Showable where
                 show (S x) = show x

Our new system can only type programs that can be written in System F.   (The tricky bit is inferring the impredicative instantiations.)


From: ghc-devs <ghc-devs-bounces at> On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena <trupill at>
Cc: GHC developers <ghc-devs at>
Subject: Re: New implementation for `ImpredicativeTypes`

I didn't say anything when you were requesting use cases, so I have no right to complain, but I'm still a little disappointed that this doesn't fix my (admittedly very minor) issue:<>

For those who don't want to click on the reddit link: I would like to be able to write something like map show ([1, 'a', "b"] :: [forall a. Show a => a]), and have it work.

On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena <trupill at<mailto:trupill at>> wrote:
Hi all,
As I mentioned some time ago, we have been busy working on a new implementation of `ImpredicativeTypes` for GHC. I am very thankful to everybody who back then sent us examples of impredicativity which would be nice to support, as far as we know this branch supports all of them! :)

If you want to try it, at<> you can find the result of the pipeline, which includes builds for several platforms (click on the "Artifacts" button, the one which looks like a cloud, to get them). The code is being developed at<>.

Any code should run *unchanged* except for some eta-expansion required for some specific usage patterns of higher-rank types. Please don't hesitate to ask any questions or clarifications about it. A merge request for tracking this can be found at<>

Kind regards,
ghc-devs mailing list
ghc-devs at<mailto:ghc-devs at><>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list