
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