A bit of hetero reading

1.hs

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}

import Data.List

data Def = Col { colName :: String }

data Val = VInt Int
         | VBool Bool

getValueIndex :: String -> [Def] -> Maybe Int
getValueIndex s = findIndex ((s ==) . colName)

getValue :: String -> [Def] -> [Val] -> Maybe Val
getValue s defs vals = (vals !!) <$>  getValueIndex s defs

class F a where fs :: Val -> Maybe a
instance F Int where {fs (VInt i) = Just i ; fs _ = Nothing}
instance F Bool where {fs (VBool b) = Just b ; fs _ = Nothing}

data S = S S | Z

data V (a::S) where
  Nil :: V 'Z
  (:.) :: String -> V a -> V ('S a)

class FV a b c | a b -> c where
  fvv :: V a -> [Def] -> [Val] -> b -> Maybe c

instance FV 'Z a a where fvv _ _ _ x = Just x

instance (F a, FV s b c) => FV ('S s) (a -> b) c where
  fvv (s :. rest) defs vals f =
    fvv rest defs vals . f =<< fs =<< getValue s defs vals

test0 = fvv ("Foo":.("Bar":.Nil))
            [Col "Bar", Col "Foo"]
            [VInt 5, VInt 7]
            ((,) @ Int @ Int)

tf-only.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

import Data.Constraint
import Data.List
import Data.Type.Bool
import Data.Type.Equality

data Def = Col { colName :: String }

data Val = VInt Int
         | VBool Bool

getValueIndex :: String -> [Def] -> Maybe Int
getValueIndex s = findIndex ((s ==) . colName)

getValue :: String -> [Def] -> [Val] -> Maybe Val
getValue s defs vals = (vals !!) <$>  getValueIndex s defs

class F a where fs :: Val -> Maybe a
instance F Int where {fs (VInt i) = Just i ; fs _ = Nothing}
instance F Bool where {fs (VBool b) = Just b ; fs _ = Nothing}

data S = S S | Z

data V (a::S) where
  Nil :: V 'Z
  (:.) :: String -> V a -> V ('S a)

type family Exq a b where
  Exq 'Z     a        = a
  Exq ('S t) (a -> b) = Exq t b

class Foo t q where
  foo :: V t -> [Def] -> [Val] -> q -> Maybe (Exq t q)
instance F a => Foo ('S 'Z) (a -> b) where
  foo (s :. Nil) df vals q = fmap q . fs =<< getValue s df vals
instance (F a, Foo ('S k) b) => Foo ('S ('S k)) (a -> b) where
  foo (s :. ss) df vals q = foo ss df vals . q =<< fs =<< getValue s df vals

test0 = foo ("Foo":.("Bar":.Nil))
            [Col "Bar", Col "Foo"]
            [VInt 5, VInt 7]
            ((,) @ Int @ Int)