Hi everyone, The proposal is to add a way to name existential type variables in pattern matches: https://github.com/ghc-proposals/ghc-proposals/pull/96. Suppose we have a constructor with an existential: data T where MkT :: forall a. Show a => a -> T Under the proposal, we could then bind that existential in a match against MkT: f :: T -> String f (MkT @a x) = show (x :: a) Note that this reuses the syntax for visible type application. Only the forms @a (where 'a' is a variable) and @_ are permitted. In the discussion the following major questions have been raised. 1. What about universally quantified type variables, such as 'a' in the following definition: data U a where MkU :: forall a b. Show a => b -> T a 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: g :: U a -> String g (MkU @b x) = show (x :: b) The bulk of the discussion was about this question. 2. What exactly is an existential? The above examples are clear but what about: type family Id a where Id a = a data T a where MkT :: forall a. a -> T (Id a) This is an existential under the current rules but given this, the distinction between existentials and universals might be not entirely intuitive. 3. What about pattern synonyms? The proposal now clarifies that they are treated exactly the same as data constructors. 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: data C a = C a h (C @Int n) = n 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. As to syntax, perhaps using 'type' or 'forall' as type binders instead of '@' would work. Thanks, Roman