#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.... #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