<div dir="ltr"><div>Hi everyone,</div><div><br></div><div>The proposal is to add a way to name existential type variables in pattern matches: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/96">https://github.com/ghc-proposals/ghc-proposals/pull/96</a>.</div><div><br></div><div>Suppose we have a constructor with an existential:</div><div><br></div><div>data T where</div><div>  MkT :: forall a. Show a => a -> T</div><div><br></div><div>Under the proposal, we could then bind that existential in a match against MkT:</div><div><br></div><div>f :: T -> String</div><div>f (MkT @a x) = show (x :: a)</div><div><br></div><div>Note that this reuses the syntax for visible type application. Only the forms @a (where 'a' is a variable) and @_ are permitted.</div><div><br></div><div>In the discussion the following major questions have been raised.</div><div><br></div><div>1. What about universally quantified type variables, such as 'a' in the following definition:</div><div><br></div><div>data U a where</div><div>  MkU :: forall a b. Show a => b -> T a</div><div><br></div><div>Do we need to mention 'a' in a pattern match against MkU? The answer (now reflected in the proposal) is no - universally quantified type variables can't be bound in this way. The pattern would look like this:</div><div><br></div><div>g :: U a -> String</div><div>g (MkU @b x) = show (x :: b)</div><div><br></div><div>The bulk of the discussion was about this question.</div><div><br></div><div>2. What exactly is an existential? The above examples are clear but what about:</div><div><br></div><div>type family Id a where Id a = a</div><div>data T a where</div><div>  MkT :: forall a. a -> T (Id a)</div><div><br></div><div>This is an existential under the current rules but given this, the distinction between existentials and universals might be not entirely intuitive.</div><div><br></div><div>3. What about pattern synonyms? The proposal now clarifies that they are treated exactly the same as data constructors.</div><div><br></div><div><br></div><div>My recommendation is to reject the proposal as is but to encourage the authors to come up with a different syntax. The reason is that the proposal "steals" the syntax for explicit type application in patterns but it seems to me that type application in patterns makes perfect sense! I don't see why I shouldn't be eventually able to write something like:</div><div><br></div><div>data C a = C a</div><div>h (C @Int n) = n</div><div><br></div><div>and have the compiler infer h :: C Int -> Int. Having @type mean something other than type application in pattern seems highly confusing to me and kills a possibly useful future feature. I believe a lot of the confusion with respect to point 1 above happened precisely because the proposal blurs the difference between type application and binding in patterns.</div><div><br></div><div>As to syntax, perhaps using 'type' or 'forall' as type binders instead of '@' would work.</div><div><br></div><div>Thanks,</div><div><br></div><div>Roman</div><div><br></div></div>