[GHC] #13159: Allow visible type application with pattern synonyms in patterns

[GHC]

#13159: Allow visible type application with pattern synonyms in patterns
-------------------------------------+-------------------------------------
           Reporter:  lexi.lambda    |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #13158
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Somewhat related to #13158, it would be nice if pattern synonyms allowed
 visible type application with the `TypeApplications` extension enabled.
 This would obviously be tricky due to the existing meaning of `@` in
 patterns, though I think it would technically be unambiguous here. Still,
 I’d understand if you didn’t want to complicate the parser that much
 further.

 The motivator, though, is that it would be nice to be able to write
 pattern synonyms with ambiguous types an explicitly instantiate them, for
 the same reason type applications are useful for terms. As mentioned in
 #13158, this would permit writing a pattern synonym to emulate case
 analysis on types:

 {{{#!hs
 {-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables,
              TypeApplications, TypeOperators, ViewPatterns #-}

 import Data.Typeable

 viewEqT :: forall b a. (Typeable a, Typeable b) => a -> Maybe ((a :~: b),
 b)
 viewEqT x = case eqT @a @b of
   Just Refl -> Just (Refl, x)
   Nothing -> Nothing

 pattern EqT :: forall b a. (Typeable a, Typeable b) => (a ~ b) => b -> a
 pattern EqT x <- (viewEqT @b -> Just (Refl, x))
 }}}

 If visible type applications were permitted in patterns, then such case
 analysis could be written like this:

 {{{#!hs
 evilId :: Typeable a => a -> a
 evilId (EqT @Int n) = n + 1
 evilId (EqT @String str) = reverse str
 evilId x = x
 }}}

 …which I think looks relatively pleasant!

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13159>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler