[Haskell-cafe] Type families and GADTs in 6.9

[Dan Doel]

Hello,

I've been playing around with type families off and on in 6.8, but, what with 
the implementation therein being reportedly incomplete, it's hard to know 
what I'm getting right and wrong, or what should work but doesn't and so on. 
So, I finally decided to take the plunge and install 6.9 (which, perhaps, 
isn't yet safe in that regard either, but, such is life :)). But, when I 
loaded up one of my programs, I got a type error. The subject is inductively 
defined tuples:

-------------------------------------

{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls, TypeOperators #-}

data Zero
data Succ n

data Nat n where
  Zero :: Nat Zero
  Succ :: Nat n -> Nat (Succ n)

data FZ
data FS a

data Fin fn n where
  FZ :: Fin FZ (Succ n)
  FS :: Fin fn n -> Fin (FS fn) (Succ n)

f0 = FZ
f1 = FS f0
f2 = FS f1
-- ... etc.

data Nil
data t ::: ts

type family Length ts :: *
type instance Length Nil = Zero
type instance Length (t ::: ts) = Succ (Length ts)

type family Lookup ts fn :: *
type instance Lookup (t ::: ts) FZ = t
type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn

infixr 4 :::

data Tuple ts where
  ZT    :: Tuple Nil
  (:::) :: t -> !(Tuple ts) -> Tuple (t ::: ts)

{-
  This type signature gets complained about in 6.8, but it seems like
  a sensible one:
    proj :: (Length ts ~ n) => Fin fn n -> Tuple ts -> Lookup ts fn
  Indexing the tuple by its length is also an option (which works).
  In any case, the code doesn't even work with the lenient 6.8 signature:
-}
proj :: Fin fn n -> Tuple ts -> Lookup ts fn
proj FZ      (v ::: vs) = v
proj (FS fn) (v ::: vs) = proj fn vs

-------------------------------------

The overall goal being Haskell-alike tuples with a single projection function 
that works for all of them, without having to use template haskell for 
instance (fst = proj f0, snd = proj f1, etc.). However, proj results in a 
type error:

    Occurs check: cannot construct the infinite type:
      t = Lookup (t ::: ts) fn
    In the pattern: v ::: vs
    In the definition of `proj': proj FZ (v ::: vs) = v

Oddly (to me), if I reverse the clauses, the compiler doesn't complain about 
the FS case, still complaining about FZ. Now, my thought process here is that 
the pattern match against FZ (the value) requires fn to be FZ (the type), 
which should tell the compiler to solve "t ~ Lookup (t ::: ts) FZ" which is, 
of course, the first instance above.

Am I doing something wrong, or have I bumped into as-yet-unimplemented 
functionality?

Thanks for your time and help.
-- Dan