[GHC] #12564: Type family in type pattern kind

[GHC]

#12564: Type family in type pattern kind
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:  14119             |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 After reading comment:13, I'm left wondering about how this idea would
 work in practice. I've wanted to define instances like these before:

 {{{#!hs
 type family Sing :: k -> Type

 type instance Sing @Type     = TypeRep
 type instance Sing @(Sing a) = Sing
 }}}

 Currently, GHC prevents me from writing the `Sing @(Sing a)` instance
 since its argument mentions the `Sing` type family. If I understand the
 plan in comment:13, then GHC would turn this instance into something that
 looks roughly like this:

 {{{#!hs
 type instance (x ~ Sing a) => Sing @x = Sing
 }}}

 However, this might be a problem. We have both a `Sing @x` and a `Sing
 @Type` instance defined—wouldn't these instances conflict?

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