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