[Haskell-cafe] Re: Type families and GADTs in 6.9

[ChrisK]

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)
> -}