[ghc-steering-committee] Proposal: Binding existential type variables (#96)

[Richard Eisenberg]

- I, too, like Joachim's proposal.

- I like Joachim's original proposal more than Simon's simplification... but Simon's simplification is indeed a simplification, which is nice.

- If we think that we might want to migrate to Joachim's proposal eventually (and I do), then I agree with his amendment to forbid shadowing.

- Joachim parenthetically mentioned the possibility of "matchable implicit arguments". We actually already have these -- they're called existential variables. What would be new is matchable /relevant/ implicit arguments, which could be matched against a pattern. Being able to match against these essentially requires Joachim's expanded proposal.

- Roman asks about `data T a = MkT`, where `a`'s kind is unrestricted. This means we have `MkT :: forall {k} (a :: k). T a`. Following the current rules for specified-vs-inferred variables, the k variable is *inferred*, meaning it is not available for type application or patterns. That doesn't change here; a user of `MkT` cannot access the `k` variable through @-signs in either context. This is unchanged by #103.

On balance, I favor Joachim's full proposal, without the simplification, but I favor Simon's simplification over the original proposal. Emma (the proposer), Stephanie, and I debated these designs at some length before asking Emma to write up the proposal. We did have a design with universals and existentials both able to be written explicitly in patterns, but we felt that having universals able to be types while existentials must be variables was awkward. Both new proposals on the floor treat universals and existentials similarly here, which is an improvement on anything that Emma, Stephanie, and I debated.

Richard

> On Mar 28, 2018, at 11:42 AM, Joachim Breitner <mail at joachim-breitner.de> wrote:
> 
> Hi,
> 
> 
> Am Mittwoch, den 28.03.2018, 16:37 +0100 schrieb Roman Leshchinskiy:
>> On Tue, Mar 27, 2018 at 6:24 AM, Joachim Breitner <mail at joachim-breitner.de> wrote:
>>> 2. The distinction between existentials and universals is oddly abrupt.
>> 
>> This is a good point. In addition to what Joachim said, universals
>> can also depend on existentials which I find weird.
>> 
>> As an aside, here is one corner case which I don't think is handled
>> in the proposal:
>> 
>> data T a where
>>  MkT :: forall a. T a
>> 
>> With -XPolyKinds, the type inferred for T is forall k (a :: k). T a.
>> Now, k is an existential but can it be bound in a pattern? The
>> proposal only mentions 2 cases: no forall and a forall that mentions
>> all type variables and neither applies here.
> 
> good point – the future of this should be addressed by
> https://github.com/ghc-proposals/ghc-proposals/pull/103
> but it would be clear to be explicit in how this will be handled in #96
> until #103 is fully in place.
> 
> Cheers,
> Joachim
> 
> 
> -- 
> Joachim Breitner
>  mail at joachim-breitner.de
>  http://www.joachim-breitner.de/
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee