| I think all reserverations would disappear if we can find a good | syntax for existential type variable that does not clash with | TypeApplication. I really don't agree. If we wrote f (?x : ?xs) = ... to signal that x and xs were binding sites, then I'd be fine with writing f (MkT @?a ?xs) = ... But we don’t. In patterns, a plain variable is a binding site. And it should be the same for types -- save that we need a way to distinguish terms from types, just as we do in terms. You should think of * the universal type args and required dictionaries, as INPUTs to the match * the existential args and value args, as OUTPUTS of the match Consider data T p where MkT :: p -> [q] -> T p f :: forall a. (Num a, Eq a) => T a -> Int f (T 3 y) = length y Here, the type 'a' and the dictionaries for (Eq a, Num a) are inputs to the match. If successful, the match binds the existential type 'q', and value argument (y :: [q]). A matcher for the pattern (T 3 y) would have a type like forall a r. (Num a, Eq a) => (forall q. [q] -> r) -> T a -> r Now, the things matched by the pattern are the arguments (both type and term arguments) to that continuation. These are what I expect to see bound. As a programmer you really do need to know which variables are existential. Without that you can't possibly know what programs are well typed. It seems so simple to me to say "we use the @ to distinguish between term and type arguments in applications; and between term and type binders in patterns". Simon | -----Original Message----- | From: ghc-steering-committee On Behalf Of Joachim Breitner | Sent: 26 March 2018 15:32 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal: Binding existential | type variables (#96) | | Hi, | | without adding much to the discussion, I agree with Roman’s sentiment | here. And maybe that is an indication that more people out there, who | are not as deep into the theory and implementation of this feature, | will be similarly surprised. | | Am Montag, den 26.03.2018, 09:24 +0000 schrieb Simon Peyton Jones: | > Also, you can readily do what you want with an ordinary type | signature | > in a pattern | > | > h (C n :: C Int) = n -- infers h :: C Int -> Int | | Isn’t that true for most uses of TypeApplications in expressions as | well, that they could readily be replaced by type signatures? And yet | we offer the TypeApplications extension? | | Here is another example where the current proposal superficially | breaks the nice equational nature of Haskell: | | data U a where MkU :: forall a b. Show a => b -> T a | | idU :: forall a. U a -> U a | idU (MkU @b x) = MkU @a @b x | | or even | | idU :: forall a. U a -> U a | idU (MkU @b x) = MkU @a x | | It is the identity! Why don’t I write the same things on both sides? | | | I think all reserverations would disappear if we can find a good | syntax for existential type variable that does not clash with | TypeApplication. | | Maybe @? instead of @ (given that ? is commonly used to refer to ∃)? | | Cheers, | Joachim | -- | Joachim Breitner | mail@joachim-breitner.de | | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.jo | achim- | breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Cecf2cfd38b0947 | 25e09d08d593265bd5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636576 | 715317265122&sdata=H5kvHXEYy9L7Pnp3CyajY9BFbhkuzHhqrxxR5xykx0M%3D&rese | rved=0

Hi, I know that it is frowned upon to discuss the merits of one proposal with hypothetical future proposals in mind, but I can’t resist: Am Montag, den 26.03.2018, 12:44 -0400 schrieb Richard Eisenberg:

3. Like Simon, I see the value in being able to say that everything that occurs in a pattern is a pattern -- that is, an output of the match.

I wonder if raising this current state to a principle blocks us from very useful future extensions. In particular, I expect that in the future we will want to be able to abstract pattern synonyms over values, and be able to do something like the following, given in infeasible syntax. pattern Nths n x <- ((!! ns) -> x) squareTenth :: [Int] -> Int squareTenth (Nths 10 x) = x*x or nths :: Int -> [a] -> a nths n (Nths n x) = x Ah, and of course view patterns already break the rule that “everything that occurs in a pattern is a pattern”! So somewhere down the line, I expect that patterns with have both INPUT and OUTPUT terms, and I will be able to specify both. In the same vain, I would like to be able to specify both INPUT and OUTPUT types now. And just in case this is a course of confusion: Nobody proposes to _bind_ universal variables. But Romand and me are missing a way of explicitly _instantiating_ universal variables. The proposal only discuss the former (which I agree is bogus), but not the latter. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Hi, Am Montag, den 26.03.2018, 14:34 -0400 schrieb Richard Eisenberg:

Bringing this back to the proposal at hand, we would say this to mention a universal:

g (Just *@Int x) = x

and that would mean g :: Maybe Int -> Int

Yes! Something like that and I would fully support the proposal. But

Of course, these little syntactic sigils make Haskell look more Perlish, and that's not a good thing.

is spot-on, and finding a good syntax is the hard part here. And once we have syntax to instantiate universals and bind existentials, there is the question, which of these two deserves @ and which has to get the yet-to-be-found other one. (Personally, I’d say that @ should instantiate universals, for consistency with TypeApplications, but will not insist on this point.) Somewhat tangentially, how much should it worry us that according to the current proposal, in type Id a = a data Foo a where MkFoo :: forall a, a -> Foo a data Foo' a where MkFoo' :: forall a, a -> Foo (Id a) the constructors MkFoo and MkFoo' behave totally different wrt universals and existentials? I see the technical justification for it, but it still feels odd and unsmooth. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

On Mon, Mar 26, 2018 at 9:28 PM, Richard Eisenberg wrote:

...

On Mar 26, 2018, at 2:43 PM, Joachim Breitner wrote:

...

And once we have syntax to instantiate universals and bind existentials, there is the question, which of these two deserves @ and which has to get the yet-to-be-found other one. (Personally, I’d say that @ should instantiate universals, for consistency with TypeApplications, but will not insist on this point.)

And I'd say that @ should bind existentials, for consistency with the usual default for patterns, which is the "output" mode. Besides, I think binding existentials will be much more common than instantiating universals.

The point about inputs vs. outputs to patterns has clarified things a lot for me, thanks! I think that if we ever want to allow inputs to patterns, we could just use a reserved token to separate those (assuming all inputs come before the outputs). Something like this (\ already means "here come binders"): C <inputs> \ <outputs> Then @ would instantiate universals before \ and bind existentials after and \ could be omitted if there are no inputs, thus subsuming the current pattern syntax. In any event, this convinces me that we won't be irrevocably taking away syntax which might prove essential in the future and I now support the proposal. Roman

Hi, I was close to writing “I am not convinced, but if I am the only one who is unhappy with the current proposal, then I will not stand in the way”. But I was away from the computer, so I could not write that, and so I pondered the issue some more, and the more I ponder it, the more dissatisfied with that outcome I am (and it kept me awake tonight…). But I want to be constructive, so I am offering an alternative proposal. Still half-baked, of course, but hopefully already understandable and useful. ### What are the issues? But first allow me to summarize the points of contention, collecting the examples that I brought up before, and adding some new ones. 1. It breaks equational reasoning. data T a where MkT :: forall a b. b -> T a foo (MkT @a y) = E[a :: y] bar = C[foo (MkT @Int True)] is different from bar = C[E[True :: Int]] While we can certainly teach people the difference between @ in expression and @ in patterns, I find this a high price to pay. 2. The distinction between existentials and universals is oddly abrupt. data A a where MkA :: forall a. A a has a universal, but data A' a where MkA' :: forall a. A (Id a) has an extensional. Also, every universal can be turned into an existential, by introducing a new universal. a is universal in A, but existential in data A'' a where MkA'' :: forall a b. a ~ b -> A b although it behaves pretty similar. 3. The intuition “existential = Output” and “universal = Input” is not as straight-forward as it first seems. I see how data B where MkB :: forall a. B has an existential that is unquestionably an output of the pattern match. But what about data B2 where MkB2 :: forall a b. a ~ b -> B now if I pattern match (MkB2 @x @y), then yes, “x” is an output, but “y” somehow less so. Relatedly, if I write data B3 where MkB3 :: forall a. a ~ Int -> B then it’s hardly fair to say that (MkB3 @x) outputs a type “x”. And when we have data B4 a where MkB4 :: forall a b. B (a,b) then writing (MkB4 @x @y) also does not really give us a new types stored in the constructor, but simply deconstructs the type argument of B4. ### Goals of the alternative proposal So is there a way to have our cake and eat it too? A syntax that A. allows us to bind existential variables, B. has consistent syntax in patterns and expressions and C. has the desired property that every variable in a pattern is bound there? Maybe there is. The bullet point 3. above showed that thinking in terms of Input and Output – while very suitable when we talk about the term level – is not quite suitable on the Haskell type level, where information flows in many ways and direction. A better way of working with types is to think of type equalities, unification and matching. And this leads me to ### The alternative proposal (half-baked) Syntax: Constructors in pattern may have type arguments, using the @ syntax from TypeApplication. The type argument correspond to _all_ the universally quantified variables in their type signature. Scoping: Any type variable that occurs in a pattern is brought into scope by this pattern. If a type variable occurs multiple times in the same pattern, then it is the still same variable (no shadowing within a pattern). Semantics: (This part is still a bit vague, if it does not make sense to you, then better skip to the examples.) Consider a constructor C :: forall a b. Ctx[a,b] => T (t2[a,b]) If we use use this in a pattern like so (C @s1 @s2) (used at some type T t) where s1 and s2 are types mentioning the type variables x and y, then this brings x and y into scope. The compiler checks if the constraints from the constructor C', namely (t ~ t2[a,b], Ctx[a,b]) imply that a and b have a shape that can be matched by s1 and s2. If not, then a type error is reported. If yes, then this matching yields instantiations for x and y. Note that this description is completely independent of whether a or b actually occur in t2[a,b]. This means that we can really treat all type arguments of C in a consistent way, without having to put them into two distinct categories. One could summarize this idea as making these two changes to the original proposal: + Every variable is an existential (in that proposal’s lingo) + We allow type patterns in the type applications in patterns, not just single variables. ### Examples Let's see how this variant addresses the dubious examples above. * We now write data T a where MkT :: forall a b. b -> T a foo (MkT @_ @a y) = E[a :: y] bar = C[foo (MkT @Int True)] which makes it clear that @a does not match the @Int, but rather an implicit parameter. If the users chooses to be explicit and writes it as bar = C[foo (MkT @Int @Bool True)] then equational reasoning worksand gives us bar = C[E[True :: Bool]] * The difference between data A a where MkA :: forall a. A a data A' a where MkA' :: forall a. A (Id a) data A'' a where MkA'' :: forall a b. a ~ b -> A b disappears, as all behave identical in pattern matches: foo, foo', foo'' :: A Integer -> () foo (MkA @x) = … here x ~ Integer … foo' (MkA' @x) = … here x ~ Integer … foo'' (MkA'' @x) = … here x ~ Integer … * Looking at data B where MkB :: forall a. B data B2 where MkB2 :: forall a b. a ~ b -> B data B3 where MkB3 :: forall a. a ~ Int -> B data B4 a where MkB4 :: forall a b. B (a,b) we can write foo (MkB @x) = … x is bound … to match the existential, as before, and foo (MkB @(Maybe x)) = would fail, as expected. We can write bar (MkB2 @x @y) = … x and y are in scope, and x~z … just as in the existing proposal, but it would also be legal to write, should one desire to do so, bar (MkB2 @x @x) = With B3 we can match this (fixed) existential, if we want. Or we can assert it’s value: baz (MkB3 @x) = … x in scope, x ~ Int … baz (MkB3 @Int) = … With B4, this everything works just as expected: quux :: B4 ([Bool],()) quux (MkB4 @x @y) = … x and y in scope, x ~ [Bool], y ~ () which, incidentially, is equivalent to the existing quux (MkB4 :: (x, y)) = … x and y in scope, x ~ [Bool], y ~ () and the new syntax also allows quux' (MkB4 @[x]) = … x in scope, x ~ Bool ### A note on scoping Above I wrote “every type variable in a pattern is bound there”. I fear that this will be insufficient when people want to mention a type variable bound further out. So, as a refinement of my proposal, maybe the existing rules for Pattern type signatures (https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...) should apply: “a pattern type signature may mention a type variable that is not in scope; in this case, the signature brings that type variable into scope” In this variant, all my babbling above can be understood as merely the natural combination of the rules of ScopedTypeVariables (which brought signatures to patterns) and TypeApplications (which can be understood as an alternative syntax for type signatures). What if I really want to introduce a new type variable x, even if x might be in scope? Well, I could imagine syntax for that, where we can list explicitly bound type variables for each function equation. data C a where MkC1 :: forall a, a -> C a MkC2 :: forall b, b -> C Int foo :: forall a. a -> C a -> () foo x c = bar c where bar (MkC1 @a) = … -- matches the a bound by foo with the argument to MkC1 -- which succeeds forall a. bar (MkC2 @a) = x -- introduces a fresh a, bound to MkC2’s existential argument -- and shadowing foo’s type variable a Ok, that ended up quite long. I guess there is a strong risk that I am describing something that Emmanuel, Simon and Richard have already thought through and discarded… if so: why was it discarded? And if not: does this proposal have merits? Cheers and good night, Joachim PS: Happy 3rd anniversary to GHC-7.10 :-) -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Hi, Am Dienstag, den 27.03.2018, 21:53 +0000 schrieb Simon Peyton Jones:

Interesting idea from Joachim. But it's quite complicated. Here is a much simpler version.

great! I like it: It is no less expressive than the original proposal, but forward-compatible to the full version of my proposal (which allows types, not just type variables). I believe we will want the full version eventually (Both to say `foo (Nothing @Int) = …` and once we have matchable implicit argument – right, Richard?), but we don’t have to do both steps at once. May I add one constraint to the simpler alternative proposal: It is an error to @-bind a type variables that would shadow type variable that is already in scope (whether from ScopedTypeVariables, from an instance head or from a @-binder). Why? Well, for forward compatibility. But also for consistency! To our users (or, at least to me) these two expressions are different ways of writing the same things: foo1, foo1' :: forall a. a -> Int foo1 x = length (Nothing :: Maybe a) foo1' x = length (Nothing @ a) I.e. TypeApplication is just a more convenient alternative to type signatures. The same is true, in patterns, under your simplified alternative proposal: foo2, foo2' :: a -> Maybe Int -> Int foo2 _ (Nothing :: Maybe a) = 42 foo2' _ (Nothing @ a) = 42 In both forms, a is bound by the pattern (and `a ~ Int` is added to the context). But note that a change somewhere else (and it could be arbitrarily far away if `foo2` is a local function) breaks the symmetry, at least with ScopedTypeVariables enabled: foo3, foo3' :: forall a. a -> Maybe Int -> Int foo3 _ (Nothing :: Maybe a) = 42 -- type error (a ≠ Int) foo3' _ (Nothing @ a) = 42 -- shadows a Hence I would ask to simply forbid the latter form in the simplified version of the proposal. This * helps the user not shooting in his own leg and * is compatible with the full proposal, where foo3 and foo3' would be equivalent. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

I can’t say that I am sure of the details, but Joachim’s proposal seems appealing to me. Manuel

Am 27.03.2018 um 16:24 schrieb Joachim Breitner :

Hi,

I was close to writing “I am not convinced, but if I am the only one who is unhappy with the current proposal, then I will not stand in the way”. But I was away from the computer, so I could not write that, and so I pondered the issue some more, and the more I ponder it, the more dissatisfied with that outcome I am (and it kept me awake tonight…).

But I want to be constructive, so I am offering an alternative proposal. Still half-baked, of course, but hopefully already understandable and useful.

### What are the issues?

But first allow me to summarize the points of contention, collecting the examples that I brought up before, and adding some new ones.

1. It breaks equational reasoning.

data T a where MkT :: forall a b. b -> T a foo (MkT @a y) = E[a :: y] bar = C[foo (MkT @Int True)]

is different from

bar = C[E[True :: Int]]

While we can certainly teach people the difference between @ in expression and @ in patterns, I find this a high price to pay.

2. The distinction between existentials and universals is oddly abrupt.

data A a where MkA :: forall a. A a

has a universal, but

data A' a where MkA' :: forall a. A (Id a)

has an extensional.

Also, every universal can be turned into an existential, by introducing a new universal. a is universal in A, but existential in

data A'' a where MkA'' :: forall a b. a ~ b -> A b

although it behaves pretty similar.

3. The intuition “existential = Output” and “universal = Input” is not as straight-forward as it first seems. I see how

data B where MkB :: forall a. B

has an existential that is unquestionably an output of the pattern match. But what about

data B2 where MkB2 :: forall a b. a ~ b -> B

now if I pattern match (MkB2 @x @y), then yes, “x” is an output, but “y” somehow less so. Relatedly, if I write

data B3 where MkB3 :: forall a. a ~ Int -> B

then it’s hardly fair to say that (MkB3 @x) outputs a type “x”. And when we have

data B4 a where MkB4 :: forall a b. B (a,b)

then writing (MkB4 @x @y) also does not really give us a new types stored in the constructor, but simply deconstructs the type argument of B4.

### Goals of the alternative proposal

So is there a way to have our cake and eat it too? A syntax that A. allows us to bind existential variables, B. has consistent syntax in patterns and expressions and C. has the desired property that every variable in a pattern is bound there?

Maybe there is. The bullet point 3. above showed that thinking in terms of Input and Output – while very suitable when we talk about the term level – is not quite suitable on the Haskell type level, where information flows in many ways and direction.

A better way of working with types is to think of type equalities, unification and matching. And this leads me to

### The alternative proposal (half-baked)

Syntax: Constructors in pattern may have type arguments, using the @ syntax from TypeApplication. The type argument correspond to _all_ the universally quantified variables in their type signature.

Scoping: Any type variable that occurs in a pattern is brought into scope by this pattern. If a type variable occurs multiple times in the same pattern, then it is the still same variable (no shadowing within a pattern).

Semantics: (This part is still a bit vague, if it does not make sense to you, then better skip to the examples.) Consider a constructor

C :: forall a b. Ctx[a,b] => T (t2[a,b])

If we use use this in a pattern like so

(C @s1 @s2) (used at some type T t)

where s1 and s2 are types mentioning the type variables x and y, then this brings x and y into scope. The compiler checks if the constraints from the constructor C', namely (t ~ t2[a,b], Ctx[a,b]) imply that a and b have a shape that can be matched by s1 and s2. If not, then a type error is reported. If yes, then this matching yields instantiations for x and y.

Note that this description is completely independent of whether a or b actually occur in t2[a,b]. This means that we can really treat all type arguments of C in a consistent way, without having to put them into two distinct categories.

One could summarize this idea as making these two changes to the original proposal: + Every variable is an existential (in that proposal’s lingo) + We allow type patterns in the type applications in patterns, not just single variables.

### Examples

Let's see how this variant addresses the dubious examples above.

* We now write

data T a where MkT :: forall a b. b -> T a foo (MkT @_ @a y) = E[a :: y] bar = C[foo (MkT @Int True)]

which makes it clear that @a does not match the @Int, but rather an implicit parameter. If the users chooses to be explicit and writes it as bar = C[foo (MkT @Int @Bool True)] then equational reasoning worksand gives us bar = C[E[True :: Bool]]

* The difference between

data A a where MkA :: forall a. A a data A' a where MkA' :: forall a. A (Id a) data A'' a where MkA'' :: forall a b. a ~ b -> A b

disappears, as all behave identical in pattern matches:

foo, foo', foo'' :: A Integer -> () foo (MkA @x) = … here x ~ Integer … foo' (MkA' @x) = … here x ~ Integer … foo'' (MkA'' @x) = … here x ~ Integer …

* Looking at

data B where MkB :: forall a. B data B2 where MkB2 :: forall a b. a ~ b -> B data B3 where MkB3 :: forall a. a ~ Int -> B data B4 a where MkB4 :: forall a b. B (a,b)

we can write

foo (MkB @x) = … x is bound …

to match the existential, as before, and

foo (MkB @(Maybe x)) =

would fail, as expected. We can write

bar (MkB2 @x @y) = … x and y are in scope, and x~z …

just as in the existing proposal, but it would also be legal to write, should one desire to do so,

bar (MkB2 @x @x) =

With B3 we can match this (fixed) existential, if we want. Or we can assert it’s value:

baz (MkB3 @x) = … x in scope, x ~ Int … baz (MkB3 @Int) = …

With B4, this everything works just as expected:

quux :: B4 ([Bool],()) quux (MkB4 @x @y) = … x and y in scope, x ~ [Bool], y ~ ()

which, incidentially, is equivalent to the existing

quux (MkB4 :: (x, y)) = … x and y in scope, x ~ [Bool], y ~ ()

and the new syntax also allows

quux' (MkB4 @[x]) = … x in scope, x ~ Bool

### A note on scoping

Above I wrote “every type variable in a pattern is bound there”. I fear that this will be insufficient when people want to mention a type variable bound further out. So, as a refinement of my proposal, maybe the existing rules for Pattern type signatures (https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...) should apply: “a pattern type signature may mention a type variable that is not in scope; in this case, the signature brings that type variable into scope”

In this variant, all my babbling above can be understood as merely the natural combination of the rules of ScopedTypeVariables (which brought signatures to patterns) and TypeApplications (which can be understood as an alternative syntax for type signatures).

What if I really want to introduce a new type variable x, even if x might be in scope? Well, I could imagine syntax for that, where we can list explicitly bound type variables for each function equation.

data C a where MkC1 :: forall a, a -> C a MkC2 :: forall b, b -> C Int

foo :: forall a. a -> C a -> () foo x c = bar c where bar (MkC1 @a) = … -- matches the a bound by foo with the argument to MkC1 -- which succeeds forall a. bar (MkC2 @a) = x -- introduces a fresh a, bound to MkC2’s existential argument -- and shadowing foo’s type variable a

Ok, that ended up quite long. I guess there is a strong risk that I am describing something that Emmanuel, Simon and Richard have already thought through and discarded… if so: why was it discarded? And if not: does this proposal have merits?

Cheers and good night, Joachim

PS: Happy 3rd anniversary to GHC-7.10 :-)

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

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/

Yes I like the "\" too. (Or some syntax separating inputs from outputs.) More specifically, I really like the possibility of specifying input values to a pattern. You can do that with view patterns - but you can't abstract over those view patterns with a pattern synonym (currently). It'd be great to be able to say pattern P n \ x <- ((\y -> if y>2*n+1 then Just y else Nothing) -> Just x) This looks pretty impenetrable, but it's using a view pattern to test if the argument is > 2n+1, and match if so. So 'n' is an input, and x is an output. I think we have to group all the inputs together and have a separator. No inter-mingling. Remember, we want the distinction to be syntactically obvious; and outputs must be variables while inputs can be arbitrary terms or types. As discussed earlier, for inputs, @ distinguishes types from terms; for outputs, @ distinguishes type binder from term binders. Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 27 March 2018 03:47 To: Roman Leshchinskiy Cc: ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] Proposal: Binding existential type variables (#96) On Mar 26, 2018, at 5:54 PM, Roman Leshchinskiy mailto:rleshchinskiy@gmail.com> wrote: C <inputs> \ <outputs> I had been trying to figure out how to get \ involved, and this is the way. Thanks! It does require that all inputs come before all outputs, which might not be true for constructors: data T a where MkT :: forall b a. b -> T a Here, `b` is an output while `a` would be an input. And in many cases constructors designed with visible type application in mind will want to put existentials ("outputs") before universals ("inputs"). If we ever did the C <inputs> \ <outputs> in the future, I suppose we could just say that such constructors will have their type variables reordered, perhaps issuing a warning if someone writes a mis-ordered constructor. In any case, I'm glad that this discussion has changed your mind about accepting this proposal. Thanks, Richard