Hi Tom, thanks a lot for your answers. It works as expected. I am building on this proposal, but I am again stuck on the following problems: - The second proposal introduces 'Content' to the 'IsSchema' type signature. Is it necessary? The problem is when I try to extend it to other types, like 'Variation' and 'Item' (see below). - I was able to implement instances (using the first proposed solution), but I am getting error on the call site (that is: on the 'main' function. The error says: ‘SchemaVal’ is a non-injective type family. I don't know how to get around it. I would appreciate if you have another look. Here is an updated example: {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} module Test where import Data.Kind import Data.Proxy import GHC.TypeLits data Content n s b = ContentRaw | ContentTable [(n, s)] | ContentBool b deriving instance (Show n, Show s, Show b) => Show (Content n s b) data Variation n s b = Element n (Content n s b) | Group [Item n s b] deriving instance (Show n, Show s, Show b) => Show (Variation n s b) data Item n s b = Spare n | Item s (Variation n s b) deriving instance (Show n, Show s, Show b) => Show (Item n s b) -- Convert from types to values. class IsSchema t where type SchemaVal t :: Type schema :: SchemaVal t -- Instances implementation... -- to be defined... -- Test type V1 = 'Element 1 'ContentRaw type I1 = 'Item "title1" V1 type I2 = 'Item "title2" V1 type G0 = 'Group '[] type G1 = 'Group (I1 ': '[]) type G2 = 'Group (I1 ': I2 ': '[]) main :: IO () main = do print $ schema @V1 print $ schema @I1 print $ schema @I2 print $ schema @G0 print $ schema @G1 print $ schema @G2 print (schema @G1 /= schema @G2)