FieldType

errors

[1 of 1] Compiling Main             ( fieldtype.hs, fieldtype.o )

fieldtype.hs:19:27: error:
    • Expected kind ‘Fin (FieldCount T)’,
        but ‘'FZ’ has kind ‘Fin ('S n0)’
    • In the second argument of ‘FieldType’, namely ‘FZ’
      In the type instance declaration for ‘FieldType’

fieldtype.hs:20:28: error:
    • Expected kind ‘Fin (FieldCount T)’,
        but ‘'FS 'FZ’ has kind ‘Fin ('S ('S n0))’
    • In the second argument of ‘FieldType’, namely ‘FS FZ’
      In the type instance declaration for ‘FieldType’

fieldtype.hs:21:28: error:
    • Expected kind ‘Fin (FieldCount T)’,
        but ‘'FS ('FS 'FZ)’ has kind ‘Fin ('S ('S ('S n0)))’
    • In the second argument of ‘FieldType’, namely ‘FS (FS FZ)’
      In the type instance declaration for ‘FieldType’

fieldtype.hs

{-# LANGUAGE TypeInType, GADTs, TypeFamilies #-}

import Data.Kind (Type)

data N = Z | S N

data Fin :: N -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

type family FieldCount (t :: Type) :: N

type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type

data T

type instance FieldCount T = S (S (S Z))

type instance FieldType T FZ = Int
type instance FieldType T (FS FZ) = Bool
type instance FieldType T (FS (FS FZ)) = String