[Haskell-cafe] ambiguous type variable question

[Tom Ellis]

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"