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

30 Aug 2016

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

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler