[GHC] #11350: Allow visible type application in patterns

[GHC]

#11350: Allow visible type application in patterns
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
                                     |  TypeApplications PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11385            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 [https://github.com/ghc-proposals/ghc-
 proposals/pull/16#issuecomment-253612659 comment]

 {{{#!hs
 dynHead :: Dynamic -> Maybe Dynamic
 dynHead (Dyn (rxs :: TypeRep txs) (xs :: txs)) = do
   App rl rx <- splitApp rxs
   Refl <- rl `eqT` (typeRep :: TypeRep [])
   return (Dyn rx (head xs))
 }}}

 can be written as (I'm not sure about the `Con` definition)

 {{{#!hs
 pattern (:<->:) :: () => fa ~ f a => TypeRep f -> TypeRep a -> TypeRep fa
 pattern f :<->: a <- (splitApp -> Just (App f a))
   where f :<->: a = TypeApp f a

 pattern Con :: forall (u :: k1) (b :: k2). TypeRep u => u ~~ b => TypeRep
 b
 pattern Con <- (eqT (typeRep @k1 @u) -> Just HRefl)
   where Con = typeRep @k1 @u

 pattern :: () => [Int] ~~ t => TypeRep t
 pattern ListInt = Con @_ @[] :<->: Con @_ @Int
 }}}

 that should work the same as

 {{{#!hs
 pattern Int :: () => Int ~~ int => T int
 pattern Int <- (eqT (ty @Type @Int) -> Just HRefl)
   where Int = typeRep

 pattern List :: () => [] ~~ list => T list
 pattern List <- (eqT (ty @(Type -> Type) @[]) -> Just HRefl)
   where List = typeRep

 pattern :: () => [Int] ~~ t => TypeRep t
 pattern ListInt = List :<->: Int
 }}}

 Should also be able to be defined (?)

 {{{#!hs
 pattern Int :: () => Int ~~ int => T int
 pattern Int = Con @Type @Int

 pattern List :: () => [] ~~ list => T list
 pattern List = Con @(Type -> Type) @[]
 }}}

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