The length calculation looked complicated. So I reformulated it as a comparison using HasIndex. But ghc-6.8.2 was not inferring the recursive constraint on proj, so I split proj into proj_unsafe without the constraint and proj with the constraint checked only once. I also renamed ZT to Nil to be more consistent.
-- works in ghc 6.8.2 {-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls, TypeOperators #-}
data FZ data FS a
data Fin fn where FZ :: Fin FZ FS :: Fin fn -> Fin (FS fn)
f0 = FZ f1 = FS f0 f2 = FS f1 -- ... etc.
data Nil data t ::: ts
infixr 4 :::
data Tuple ts where Nil :: Tuple Nil (:::) :: t -> !(Tuple ts) -> Tuple (t ::: ts)
data HTrue
type family Lookup ts fn :: * type instance Lookup (t ::: ts) FZ = t type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn
type family HasIndex ts fn :: * type instance HasIndex (t ::: ts) FZ = HTrue type instance HasIndex (t ::: ts) (FS fn) = HasIndex ts fn
{-# INLINE proj #-} proj :: (HasIndex tsT fnT ~ HTrue) => Fin fnT -> Tuple tsT -> Lookup tsT fnT proj = proj_unsafe where proj_unsafe :: Fin fnT -> Tuple tsT -> Lookup tsT fnT proj_unsafe (FS fn) (_v ::: vs) = proj_unsafe fn vs proj_unsafe FZ (v ::: _vs) = v proj_unsafe _ Nil = error "Cannot proj Nil in proj_unsafe"
fst' :: (HasIndex ts FZ ~ HTrue) => Tuple ts -> Lookup ts FZ fst' = proj f0
snd' :: (HasIndex ts (FS FZ) ~ HTrue) => Tuple ts -> Lookup ts (FS FZ) snd' = proj f1
pair :: Tuple (Char ::: (() ::: Nil)) pair = 'a' ::: () ::: Nil
q1 :: Char q1 = fst' pair
q2 :: () q2 = snd' pair
{- This won't compile
q2 :: () q2 = snd' ('a' ::: Nil) -}