cofc.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module Test where

data HList xs where
  Nil :: HList '[]
  (:>) :: a -> HList xs -> HList (a ': xs)

infixr 9 :>

data T1 = T1 Int Char

foo :: Functor f => (Int -> f Int) -> T1 -> f T1
foo f s =     let x = case s of { T1 a b -> a :> b :> Nil }
              in fmap (\v -> case x of { _ :> vs -> T1 v (case vs of { v2 :> _ -> v2 }) })
                      (f (case x of {v1 :> _ -> v1}))

data HList2 where
  Nil2 :: HList2
  (:>>) :: Int -> HList2 -> HList2

infixr 9 :>>

data T2 = T2 Int Int

foo2 :: Functor f => (Int -> f Int) -> T2 -> f T2
foo2 f s =     let x = case s of { T2 a b -> a :>> b :>> Nil2 }
              in fmap (\v -> case x of { _ :>> vs -> T2 v (case vs of { v2 :>> _ -> v2 }) })
                      (f (case x of {v1 :>> _ -> v1}))