[GHC] #12553: Reference kind in a type instance declaration defined in another instance declaration

[GHC]

#12553: Reference kind in a type instance declaration defined in another instance
declaration
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
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):

 Recall that type families don't really have a kind because they must
 always appear saturated. I'll write `~>` for a function argument that must
 always be provided.

 (In the language of my [https://github.com/goldfirere/thesis
 dissertation], `->` used in a kind is ''matchable'' and I will use `~>`
 for ''unmatchable''. Currently, unmatchable functions in types must always
 appear saturated. Type families are the only way to write an unmatchable
 function in a type.)

 So, with

 {{{
 class Syntactic a where
   type Domain   a :: Sig u -> Type
   type Internal a :: u
 }}}

 I would expect

 {{{
 Domain :: forall u. Type ~> Sig u -> Type
 Internal :: forall u. Type ~> u
 }}}

 Having the `forall` out front does matter, because it means the type
 family can branch on the choice of `u`. (It should really be a `pi`. And
 be unmatchable.)

 If Jack wants things to be different, then he can specify

 {{{
 class Syntactic' a where
   type Domain'   a :: forall u. Sig u -> Type
   type Internal' a :: forall u. u
 }}}

 yielding

 {{{
 Domain' :: Type ~> forall u. Sig u -> Type
 Internal' :: Type -> forall u. u
 }}}

 These `forall`s describe arguments that ''cannot'' be matched against in
 the type family instances and so are seemingly less useful.

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