The problem with mult is that k is not specified unambiguously. You either need v to determine k (which is probably not what you want, at a guess), mult to take a dummy argument that determines what k is: [...] or, to make Tensor a data family instead of a type family. What is the difference making it work? The problem is that in your definition of mult mult :: Tensor k v v -> v you seem to expect the type v to be determined by the type of Tensor you apply it to. However, since Tensor is not an injective type functor, it does not uniquely determine the type v. It is possible
Paolo, that there is a completely unrelated type instance for Tensor, for different types k and v that is also equal to the type you apply mult to. If you make Tensor a data family, then the types k and v are uniquely determined, because then it is an injective type functor.
However, it would make more sense to have it be a type family, without the overhead of data (both in space and in typing).
You can make Tensor a data family and use "newtype instances". As I understand these, there should not be a space overhead. The only overhead I would expect this to introduce is the extra newtype constructor.
Is there a non- hacky approach, without dummies and without making Tensor a data family without a semantic need?
Without thinking about your problem domain, I have the impression that you do have a semantic need, because you seem to expect your Tensor type to uniquely determine at least the type v. If this is not the case, you need a different solution. Anyway, the below compiles fine with the following result: *Main> mult $ Tensor $ (V [(T [1] [2],3)] :: Vect Integer (TensorBasis [Int] [Int])) V [([1,2],3)] {-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-} {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-} data Vect k b = V [(b,k)] deriving (Eq,Show) data TensorBasis a b = T a b deriving (Eq, Ord, Show) data family Tensor k u v :: * newtype instance Tensor k (Vect k a) (Vect k b) = Tensor (Vect k (TensorBasis a b)) class Algebra k v where -- "v is a k-algebra" unit :: k -> v mult :: Tensor k v v -> v instance Algebra Integer (Vect Integer [Int]) where unit 0 = V [] unit x = V [([],x)] mult (Tensor (V ts)) = V [(g++h,x) | (T g h, x) <- ts]