[Haskell-cafe] ambiguous type variable question

[Tom Ellis]

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