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 <[email protected]> wrote: > > Why would you infer this type as opposed to `[exists a. a]`? > > On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov > <[email protected]> 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 _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
