[Haskell-cafe] ambiguous type variable question
Tom Ellis
tom-lists-haskell-cafe-2023 at jaguarpaw.co.uk
Tue Oct 10 17:40:14 UTC 2023
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"
More information about the Haskell-Cafe
mailing list