Reference kind in a type instance declaration defined in another instance declaration
Old code:
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
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:
-- • 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)?
type Domain a :: forall k. Sig k -> Type
- *Edit**: This doesn't work.