On Tue, Oct 10, 2023 at 10:45:00AM +0000, Zoran Bošnjak wrote:

I want to convert a type level structure to the value level structure of the same shape. This is the simplified example: [...] If I remove the type parameter 'b', 'ContentBool b' and coresponding 'Bool' from the sample, the conversion works as expected.

The problem is that you have constraints IsSchema ('ContentTable ts) and SchemaVal ('ContentTable ts) but `ContentTable ts` is of kind `Content n s b` , for some `n` , `s` and `b`. The instance is claiming that it works for all `b` , but it doesn't! Your instance only works when the `ContentTable ts` is of kind `Content Nat Symbol Bool`. The `b` is invisible in the type siganture so it's hard to see that it is the problem! In fact it's really weird because you'll get errors like Could not deduce SchemaVal (ContentTable ts) ~ Content Integer String Bool from the context: SchemaVal (ContentTable ts) ~ Content Integer String Bool which look like they should immediately be satisfied! Instead what it means is Could not deduce SchemaVal (ContentTable ts :: Content n s b) ~ Content Integer String Bool from the context: SchemaVal (ContentTable ts :: Content Nat Symbol Bool) ~ Content Integer String Bool Fixing `b` solves the problem, for example: instance ( IsSchema ('ContentTable ts :: Content Nat Symbol Bool), t ~ '(n, s), KnownNat n, KnownSymbol s, SchemaVal ('ContentTable ts :: Content Nat Symbol Bool) ~ Content Integer String Bool ) => IsSchema ('ContentTable (t ': ts)) where type SchemaVal ('ContentTable (t ': ts)) = Content Integer String Bool schema = case schema @('ContentTable ts :: Content Nat Symbol Bool) of ContentTable lst -> let n = natVal (Proxy @n) s = symbolVal (Proxy @s) in ContentTable ((n, s) : lst) _ -> error "internal error" Tom

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)

I am including the instances. The error is: • Couldn't match expected type: SchemaVal G1 with actual type: SchemaVal G2 NB: ‘SchemaVal’ is a non-injective type family The type variables ‘b3’, ‘b2’ are ambiguous • In the second argument of ‘(/=)’, namely ‘schema @G2’ In the first argument of ‘print’, namely ‘(schema @G1 /= schema @G2)’ In a stmt of a 'do' block: print (schema @G1 /= schema @G2) {-# 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 instance IsSchema 'ContentRaw where type SchemaVal ContentRaw = Content Integer String Bool schema = ContentRaw instance IsSchema ('ContentTable '[]) where type SchemaVal (ContentTable '[]) = Content Integer String Bool schema = ContentTable [] instance ( IsSchema ('ContentTable ts :: Content Nat Symbol Bool) , t ~ '(n, s) , KnownNat n , KnownSymbol s , SchemaVal ('ContentTable ts :: Content Nat Symbol Bool) ~ Content Integer String Bool ) => IsSchema ('ContentTable (t ': ts)) where type SchemaVal ('ContentTable (t ': ts)) = Content Integer String Bool schema = case schema @('ContentTable ts :: Content Nat Symbol Bool) of ContentTable lst -> let n = natVal (Proxy @n) s = symbolVal (Proxy @s) in ContentTable ((n, s) : lst) _ -> error "internal error" instance IsSchema 'True where type SchemaVal 'True = Bool schema = True instance IsSchema 'False where type SchemaVal 'False = Bool schema = False instance ( IsSchema b , SchemaVal b ~ Bool ) => IsSchema ('ContentBool b) where type SchemaVal ('ContentBool b) = Content Integer String Bool schema = ContentBool (schema @b) instance ( KnownNat n , SchemaVal c ~ Content Integer String Bool , IsSchema c ) => IsSchema ('Element n c) where type SchemaVal ('Element n c) = Variation Integer String Bool schema = Element (natVal (Proxy @n)) (schema @c) instance IsSchema ('Group '[]) where type SchemaVal ('Group '[]) = Variation Integer String Bool schema = Group [] instance ( IsSchema t , IsSchema ('Group ts) , SchemaVal t ~ Item Integer String Bool , SchemaVal ('Group ts :: Variation Nat Symbol Bool) ~ Variation Integer String Bool ) => IsSchema ('Group (t ': ts)) where type SchemaVal ('Group (t ': ts)) = Variation Integer String Bool schema = case schema @('Group ts) of Group lst -> Group (schema @t : lst) _ -> error "internal error" instance (KnownNat n) => IsSchema ('Spare n) where type SchemaVal ('Spare n) = Item Integer String Bool schema = Spare (natVal $ Proxy @n) instance ( KnownSymbol s , IsSchema v , SchemaVal v ~ Variation Integer String Bool ) => IsSchema ('Item s v) where type SchemaVal ('Item s v) = Item Integer String Bool schema = Item (symbolVal $ Proxy @s) (schema @v) -- Test type C = 'ContentRaw type V1 = 'Element 1 C 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 @C print $ schema @('ContentBool 'True) print $ schema @V1 print $ schema @I1 print $ schema @I2 print $ schema @G0 print $ schema @G1 print $ schema @G2 print (schema @G1 /= schema @G2)

type C = 'ContentRaw :: Content Nat Symbol Bool

This works. Thanks for your help.