| You can to do this with GADTs: | | data MyVec a where | MkMyVec :: (FinSet a) => Vec a -> MyVec a | | instance Monad MyVec where | return a = MkMyVec (vreturn a) | etc. | | GADTs are scheduled for version 6.4 of GHC. The version of GHC now in | CVS does not currently allow this however, see GHC bug #1097046. I'm not sure how to fix this bug, or even if it is a bug. Let me explain why. Usually GHC is reluctant to perform context reduction by applying instance declarations. Two reasons: 1. Postponing context reduction give more opportunities for sharing 2. With overlapping instance declarations, eager context reduction may select an instance declaration "too early"; later, more type information may be available. In fact, when you force context reduction by giving a type signature, GHC complains if (2) applies with its "the instance selected depends on the instantiation of x" message. Now, suppose we have f x = case x of MkMyVec x -> <rhs> where (x::MyVec a) the <rhs> gives a constraint (Foo [a]). And suppose we have instance (Eq a, MyVec a) => Foo [a] then you may say that f should get type f :: Eq a => MyVec a -> ... because the MyVec part gets discharged by the MkMyVec pattern match, leaving only the Eq a part. Fine. Now suppose there's an overlapping instance declaration for Foo, say Foo [Char]. Then GHC would decline to select the Foo [a] instance, so we'd infer the type f :: Foo [a] => MyVec a -> .... There would be no error message in either case, just a different type inferred. A programmer might well find this odd. Sometimes the MyVec constraints are handled by the MkMyVec constructor, and sometimes they aren't. The root of the difficulty is that the MkMyVec constructor captures constraints that mention no existentially-quantified type variable, so it'd make perfect sense to float them outwards. (In contrast, constraints mentioning existentially-quantified type variables *must* be dealt with at the pattern match.) Here's one idea. If you specify a type signature for 'f' then matters are much clearer. In my example, if you specify f :: Eq a => MyVec a -> ... then it's absolutely clear what constraints are available at the pattern match (namely Eq a, MyVec a), and we solve all the constraints there. So the rule would be: constraints are always solved *lazily* when inferring, so we'd infer f :: Foo [a] => MyVec a -> ... even without any overlap but they are solved *eagerly* when checking against a user-supplied type sig so when checking f :: Eq a => MyVec a => ... we'd accept the program. (If there were overlapping instances, we'd complain about them.) But I suspect that programmers will prefer a more woolly rule that does as much constraint solving as it can (provided all instance selection is uniquely determined). That would give the slightly surprising behaviour I describe above if an overlapping instance declaration was added. Thoughts anyone? Simon