[Haskell-cafe] ambiguous type variable question

[Zoran Bošnjak]

I am including the instances. The error is:

    • Couldn't match expected type: SchemaVal G1
                  with actual type: SchemaVal G2
      NB: ‘SchemaVal’ is a non-injective type family
      The type variables ‘b3’, ‘b2’ are ambiguous
    • In the second argument of ‘(/=)’, namely ‘schema @G2’
      In the first argument of ‘print’, namely
        ‘(schema @G1 /= schema @G2)’
      In a stmt of a 'do' block: print (schema @G1 /= schema @G2)

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Test where

import Data.Kind
import Data.Proxy
import GHC.TypeLits

data Content n s b
  = ContentRaw
  | ContentTable [(n, s)]
  | ContentBool b

deriving instance (Show n, Show s, Show b) => Show (Content n s b)

data Variation n s b
  = Element n (Content n s b)
  | Group [Item n s b]

deriving instance (Show n, Show s, Show b) => Show (Variation n s b)

data Item n s b
  = Spare n
  | Item s (Variation n s b)

deriving instance (Show n, Show s, Show b) => Show (Item n s b)

-- Convert from types to values.
class IsSchema t where
  type SchemaVal t :: Type
  schema :: SchemaVal t

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 ('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"

instance IsSchema 'True where
  type SchemaVal 'True = Bool
  schema = True

instance IsSchema 'False where
  type SchemaVal 'False = Bool
  schema = False

instance
  ( IsSchema b
  , SchemaVal b ~ Bool
  )
  => IsSchema ('ContentBool b)
  where
  type SchemaVal ('ContentBool b) = Content Integer String Bool
  schema = ContentBool (schema @b)

instance
  ( KnownNat n
  , SchemaVal c ~ Content Integer String Bool
  , IsSchema c
  )
  => IsSchema ('Element n c)
  where
  type SchemaVal ('Element n c) = Variation Integer String Bool
  schema = Element (natVal (Proxy @n)) (schema @c)

instance IsSchema ('Group '[]) where
  type SchemaVal ('Group '[]) = Variation Integer String Bool
  schema = Group []

instance
  ( IsSchema t
  , IsSchema ('Group ts)
  , SchemaVal t ~ Item Integer String Bool
  , SchemaVal ('Group ts :: Variation Nat Symbol Bool) ~ Variation Integer String Bool
  )
  => IsSchema ('Group (t ': ts))
  where
  type SchemaVal ('Group (t ': ts)) = Variation Integer String Bool
  schema = case schema @('Group ts) of
    Group lst -> Group (schema @t : lst)
    _ -> error "internal error"

instance (KnownNat n) => IsSchema ('Spare n) where
  type SchemaVal ('Spare n) = Item Integer String Bool
  schema = Spare (natVal $ Proxy @n)

instance
  ( KnownSymbol s
  , IsSchema v
  , SchemaVal v ~ Variation Integer String Bool
  )
  => IsSchema ('Item s v)
  where
  type SchemaVal ('Item s v) = Item Integer String Bool
  schema = Item (symbolVal $ Proxy @s) (schema @v)

-- Test
type C = 'ContentRaw
type V1 = 'Element 1 C
type I1 = 'Item "title1" V1
type I2 = 'Item "title2" V1

type G0 = 'Group '[]
type G1 = 'Group (I1 ': '[])
type G2 = 'Group (I1 ': I2 ': '[])

main :: IO ()
main = do
  print $ schema @C
  print $ schema @('ContentBool 'True)
  print $ schema @V1
  print $ schema @I1
  print $ schema @I2
  print $ schema @G0
  print $ schema @G1
  print $ schema @G2
  print (schema @G1 /= schema @G2)