New implementation for `ImpredicativeTypes`
vladislav at serokell.io
Fri Sep 6 21:54:18 UTC 2019
No, I don’t expect the compiler to infer existential quantification, just like it doesn’t infer higher-rank universal quantification. However, I believe we could check terms against user-written types that contain existentials.
> On 6 Sep 2019, at 23:48, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> Why would you infer this type as opposed to `[exists a. a]`?
> On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov
> <vladislav at serokell.io> wrote:
>> Alex’s example can be well-typed if we allow first-class existentials:
>> [1, ‘a’, “b”] :: [exists a. Show a => a]
>> This has nothing to do with the definition of lists. I believe the confusion was between existential types and impredicative types, as Simon has pointed out.
>> - Vlad
More information about the ghc-devs