#13042: Allow type annotations / visible type application in pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications, PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This ''is'' different. In my typical understanding of type application in patterns (forgetting about pattern synonyms for a moment), I think of type arguments only for ''existential'' type parameters. For example: {{{#!hs foo (Just @a x) = (x :: a) -- NO! `a` is universally bound bar (Just @Int x) = x -- NO! This looks like it's doing runtime type matching data E where MkE :: a -> E baz (MkE @a x) = ... -- OK. `a` is existential }}} The implicit proposal above includes visible type application for universals... but with different typing behavior than I had considered. I always thought that a pattern like `Just @Int x` would be some abominable pattern that matched against `Maybe a`, but then checked whether `a` was in fact `Int`. (This is just like how `Just True` only matches when the payload is in fact `True`.) For universals, though, there is a different typing interpretation: `Just @Int x` is a pattern against `Maybe Int`, and only `Maybe Int`. Trying to match something of type `Maybe a` against `Just @Int x` is a straightforward type error. What's challenging here is that modern patterns have arguments that go in both directions (that is, required vs provided). Normally, everything in a pattern is an output -- that is, something that is bound upon a successful pattern match. The one exception to this rule has been constructors, which are inputs. (View patterns are another way of providing inputs, which is why they are so interesting in the context of pattern synonyms.) Above is proposed adding universal type applications as inputs... an idea I think I like. A beautiful thing about adding universal type applications as inputs is that it greatly simplifies the design of type applications in patterns. I had been thinking that we allow type applications only for existential variables (as in my example above), but then the ordering of type applications might have a different meaning in a constructor expression than it would in a constructor pattern, which is very confusing. (See comment:1:ticket:11638 for further thoughts, as well as #11350 for the ticket about type applications in patterns in general.) Or have I utterly misunderstood the original post? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13042#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler