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

Hi, Am Mittwoch, den 28.03.2018, 16:37 +0100 schrieb Roman Leshchinskiy:

On Tue, Mar 27, 2018 at 6:24 AM, Joachim Breitner 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@joachim-breitner.de http://www.joachim-breitner.de/