New implementation for `ImpredicativeTypes`

[Vladislav Zavialov]

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 <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:
>> 
>> 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