GitLab

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.