Nested multiparameter classes

Question

I am trying to define a new data type containing a data type with multiple parameters (phantom types) in Haskell:

newtype Dd x y z = ToDd Cudd.Cudd.DdNode deriving (Eq,Show)

data KnowStruct a b c =
  KnS Cudd.Cudd.DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
  deriving (Eq,Show)

But this gives me the error message:

• Expected kind ‘k0 -> k1 -> *’, but ‘Dd a’ has kind ‘*’
• In the type ‘(Dd a b c)’

Why is this the case?

Is it also possible to define KnowStruct without using any requirement of context / parameter specification for the contained Dd type? e.g. :

data KnowStruct =
  KnS Cudd.Cudd.DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
  deriving (Eq,Show)

I made a function class dealing with all variations of Dds, and only use these in the functions acting on KnowStructs - so in theory there is no need to specify what kind of Dd the KnowStruct contains..

Answer 1

The first one works for me, try giving them explicit kind signatures

{-# Language DerivingStrategies       #-}
{-# Language PolyKinds                #-}
{-# Language StandaloneKindSignatures #-}

import Data.Kind

data DdManager = DdManager deriving stock (Eq, Show)
data DdNode    = DdNode    deriving stock (Eq, Show)
data Agent     = Agent     deriving stock (Eq, Show)
data Prp       = Prp       deriving stock (Eq, Show)

type    Dd :: k -> j -> i -> Type
newtype Dd x y z = ToDd DdNode
  deriving stock (Eq, Show)

type KnowStruct :: k -> j -> i -> Type
data KnowStruct a b c =
  KnS DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
  deriving stock (Eq, Show)

Is it also possible to define KnowStruct without using any requirement of context / parameter specification for the contained Dd type?

This is possible, and is called existential quantification because the type variables don't appear in the return type.

Deriving Show requires standalone deriving because of the existential quantification and Eq can't be easily derived. Since a, b, c are existentially quantified when you are comparing two KnowStructs you are comparing Dd a1 b1 c1 and Dd a2 b2 c2 with completely different type variables.

{-# Language ExistentialQuantification #-}
{-# Language StandaloneDeriving        #-}

import Data.Kind

data DdManager = DdManager deriving stock (Eq, Show)
data DdNode    = DdNode    deriving stock (Eq, Show)
data Agent     = Agent     deriving stock (Eq, Show)
data Prp       = Prp       deriving stock (Eq, Show)

-- I specialize this to some kind (`Type'). Otherwise the
-- kind would have to be an argument to `KnowStruct` below.
type    Dd :: Type -> Type -> Type -> Type
newtype Dd x y z = ToDd DdNode
  deriving stock (Eq, Show)

type KnowStruct :: Type
data KnowStruct = forall a b c.
  KnS DdManager [Prp] (Dd a b c) [(Agent,[Prp])]

deriving stock
  instance Show KnowStruct

I prefer the (equivalent) GADT syntax

{-# Language GADTs #-}

type KnowStruct :: Type
data KnowStruct where
  KnS :: DdManager -> [Prp] -> Dd a b c -> [(Agent,[Prp])] -> KnownStruct