Re: New implementation for `ImpredicativeTypes`

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. - Vlad

On 6 Sep 2019, at 23:48, Iavor Diatchki wrote:

Why would you infer this type as opposed to `[exists a. a]`?

On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov wrote:

...

Iavor,

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