
On Tue, Oct 10, 2023 at 12:34:36PM +0100, Tom Ellis wrote:
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! [...] Fixing `b` solves the problem, for example:
In fact, my favourite way of dealing with it would be as follows (I don't know why we seemingly have to indirect through SchemaVal') -- This data structure serves both for 'type level' and 'value level'. data Content n s b = ContentRaw | ContentTable [(n, s)] | ContentBool b deriving instance (Show n, Show s, Show b) => Show (Content n s b) -- Convert from types to values. type IsSchema :: forall n s' b. Content n s' b -> Constraint class IsSchema s where type SchemaVal s :: Type schema :: SchemaVal s type SchemaVal' :: forall n s b. Content n s b -> Type type SchemaVal' s = SchemaVal s 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 @Nat @Symbol @Bool ('ContentTable ts), t ~ '(n, s), KnownNat n, KnownSymbol s, SchemaVal' @Nat @Symbol @Bool ('ContentTable ts) ~ Content Integer String Bool ) => IsSchema ('ContentTable (t ': ts)) where type SchemaVal ('ContentTable (t ': ts)) = Content Integer String Bool schema = case schema @Nat @Symbol @Bool @('ContentTable ts) of ContentTable lst -> let n = natVal (Proxy @n) s = symbolVal (Proxy @s) in ContentTable ((n, s) : lst) _ -> error "internal error"