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
Then
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.)
Simon
From: ghc-devs <ghc-devs-bounces@haskell.org>
On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena <trupill@gmail.com>
Cc: GHC developers <ghc-devs@haskell.org>
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:
https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8&depth=9
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@gmail.com> wrote: