Skip to content

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.
Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information