[GHC] #13042: Allow type annotations / visible type application in pattern synonyms

[GHC]

#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