[GHC] #15658: strange inferred kind with TypeInType

[GHC]

#15658: strange inferred kind with TypeInType
-------------------------------------+-------------------------------------
        Reporter:  dmwit             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.2
      Resolution:                    |             Keywords:  TypeInType,
                                     |  GHCProposal
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * keywords:   => TypeInType, GHCProposal


Comment:

 This is expected: `TypeInType` gives programmers a limited ability to
 write dependent quantification in kinds. The
 [https://downloads.haskell.org/~ghc/8.4.3/docs/html/users_guide/glasgow_exts.html?highlight=typeintype
 #inferring-dependency-in-datatype-declarations Inferring dependency in
 datatype declarations] section of the users' guide documents this feature
 to some degree. The part that is not documented is the `forall k ->` bit,
 which I'll briefly explain here.

 Here is the type family you wrote (with explicit kinds for clarity):

 {{{#!hs
 type family F (f :: *) (a :: *) :: a
 }}}

 This binds the `f` and `a` type variables, and interestingly enough, it
 //reuses// the bound `a` type variable later in the return kind. In other
 words, `a` is used in a dependent fashion, so the kind for `F` is (again,
 with explicit kinds for clarity):

 {{{#!hs
 F :: * -> forall (a :: *) -> a
 }}}

 This kind says that `F` takes two type arguments of kind `*` and returns a
 type of kind `a`, where `a` is the second type argument. Importantly, the
 kind of `F` is //not// `* -> forall (a :: *). a`, since that would imply
 that `a` is insivible (i.e., that you don't explicitly pass it as an
 argument to `F`). You can think of the use of `->` versus `.` as
 indicating visible arguments versus invisible ones.

 As I briefly mentioned before, this aspect of kinds is not really
 documented at the moment. This is partly because while you can observe
 these kinds in GHCi (through `:kind`), you cannot write them yourself
 (they'll simply fail to parse at the moment). [https://github.com/ghc-
 proposals/ghc-proposals/pull/81 This GHC proposal] aims to rectify this.

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