[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:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

@@ -65,0 +65,2 @@
+
+ **Edit**: This doesn't work.

New description:

 Old code:

 {{{#!hs
 data Full :: Type -> Type

 data AST :: (Type -> Type) -> (Type -> Type)

 -- ASTF :: (Type -> Type) -> (Type -> Type)
 type ASTF dom a = AST dom (Full a)

 class Syntactic a where
   type Domain   a :: Type -> Type
   type Internal a :: Type
   desugar :: a -> ASTF (Domain a) (Internal a)
   sugar   :: ASTF (Domain a) (Internal a) -> a
 }}}

 ----

 New code with richer kinds

 {{{#!hs
 data Sig a = Full a | a :-> Sig a

 data AST :: (Sig a -> Type) -> (Sig a -> Type)

 data Sig a = Full a | a :-> Sig a

 -- ASTF :: (Sig a -> Type) -> (a -> Type)
 type ASTF dom a = AST dom (Full a)

 class Syntactic a where
   type Domain   a :: Sig Type -> Type
   type Internal a :: Type
   desugar :: a -> ASTF (Domain a) (Internal a)
   sugar   :: ASTF (Domain a) (Internal a) -> a
 }}}

 As the type of `ASTF` hints at it could accept arguments of kind `Sig a ->
 Type` and `a`. I would like to reference the variable `a` from the kind of
 `Domain` in the kind of `Internal`, but this fails:

 {{{#!hs
 -- • Kind variable ‘u’ is implicitly bound in datatype
 --   ‘Internal’, but does not appear as the kind of any
 --   of its type variables. Perhaps you meant
 --   to bind it (with TypeInType) explicitly somewhere?
 --   Type variables with inferred kinds: a
 -- • In the class declaration for ‘Syntactic’
 class Syntactic a where
   type Domain   a :: Sig u -> Type
   type Internal a :: u
   desugar :: a -> ASTF (Domain a) (Internal a)
   sugar   :: ASTF (Domain a) (Internal a) -> a
 }}}

 ----

 Should the `u` in the kind of `Domain a` be quantified over (which makes
 this compile)?

 {{{#!hs
   type Domain   a :: forall k. Sig k -> Type
 }}}

 **Edit**: This doesn't work.

--

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