[GHC] #11385: Unify named wildcards in different type applications

[GHC]

#11385: Unify named wildcards in different type applications
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  NamedWildCards TypeApplications    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 ([https://www.reddit.com/r/haskell/comments/4030lv/unifying_distinct_type_variables_in/
 motivating post])

 I would like to use type application to specialize

 {{{#!hs
 Sub :: forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
 Sub @(Ord _a) @(Eq _a) :: forall {a}. (Ord a => Dict (Eq a)) -> Ord a :-
 Eq a
 }}}

 and

 {{{#!hs
 map :: forall a b. (a -> b) -> [a] -> [b]
 map @_a @_a :: forall {a}. (a -> a) -> [a] -> [a]
 }}}

 Is there a fundamental reason why named wildcards are not allowed to unify
 between type applications within the same expression?
 [https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html
 #named-wildcards Documentation]:

 > These are called named wildcards. All occurrences of the same named
 wildcard within one type signature will unify to the same type.

 I don't know if this is intended.

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