Hi, I've been fidgeting with a fixed-length list library, for things like 3d vectors/points, rgba tuples, etc. The data type is data a :. b = (:.) a b deriving (everything reasonable) infixr :. Nothing in that type specifies that for the partially instantiated type t1:.t2:.t3, t1 and t2 should be equal. (Like Int:.Int:.() for a 2D integer point.) But t1 and t2 will always will be equal, at least I want them to always be equal, and everything useful I can think of needs them to be equal. (Note I won't actually store things in these data types. This is just a way of defining operations. Packed arrays and vectors will be converted to/from these types in a stream-fusioney kind of way. That's the plan, at least.) Anyway, I don't need to force them to be equal because all of the functions for these list-like things come in the form of classes, and those classes have fundeps, and the fundeps let me enforce type constraints. The problem I'm having is making these constraints work nicely with inference. I'm not sure exactly whats going on, which is why I'm asking the list. For an example, folding: -- the fold function/class class Fold a v | v -> a where fold :: (a -> a -> a) -> v -> a foldl :: (b -> a -> b) -> b -> v -> b foldr :: (a -> b -> b) -> b -> v -> b -- base case of the recursion, () is like [] instance Fold a (a:.()) where fold f (a:._) = a foldl f z (a:._) = f z a foldr f z (a:._) = f a z -- inductive case. Pick one of the "instance" declarations below... instance Fold a (a:.u) => Fold a (a:.a:.u) where -- I1 instance Fold a (a2:.u) => Fold a (a:.a2:.u) where -- I2 fold f (a:.v) = f a (fold f v) foldl f z (a:.v) = f (foldl f z v) a foldr f z (a:.v) = f a (foldr f z v) Now, both of those instance declarations work. The first one (I1) specifies that all of the list elements should be the same type, "a". The second (I2) doesn't say that right away, because one is 'a' and the other is 'a2.' However the fundep (v->a) will force a and a2 to match, so from orbit the two instances appear the same. In practice, I1 does not cause the type checker to infer the type of list elements, while I2 does. So, in ghci, if you do foldr (:) [] (1:.2:.3:.()) With I1 you'll get an error like "no instance for Fold a (t :. t1 :. t2 :. ()).." But with I2, it will infer 1 2 and 3 to all be of type "Num a => a" and will evaluate the expression to [1,2,3]. So the question is "Why?" For simple things like fold, map, etc., I can massage the instance declarations so that the type checker infers things for me, but for more complicated recursions, I'm having trouble. (For example, computing determinants by minor expansion. Not the most efficient way I know, but if I can't figure that out there's no hope for Gaussian elimination.) The functions work, its just the inference that isn't working. I'm forced to annotate things, or at least ensure that the types of the arguments can be inferred from someplace else. Scott