The problem you report can be fixed with some trickery and local functional dependencies. I'd like to show a different solution, which follows a useful general pattern, of isolating overlapping instances to one small part of the program that analyzes the type. The rest of the type program just uses the results of the analysis.

I wasn't able to find the definition of AllOf(But): It is in the complete code http://pobox.com/~oleg/ftp/Haskell/poly2.hs It isn't that interesting: data AllOfBut x y

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} {-# OPTIONS -fallow-overlapping-instances #-} module HAA where import HListPrelude data HTrue data HFalse -- If two arguments are HList's, concatenate them. If only one of them -- is HList, add the other to the head. We assume at least one is an HList. class IsHList a b | a -> b instance IsHList HNil HTrue instance IsHList (HCons a b) HTrue instance TypeCast HFalse y => IsHList x y -- The are no overlapping instances below class (HList c) => HListAppendArbitrary a b c | a b -> c where hAppendArbitrary :: a -> b -> c instance (IsHList a af, IsHList b bf, HAA af bf a b c) => HListAppendArbitrary a b c where hAppendArbitrary = haa (undefined::af) (undefined::bf) class (HList c) => HAA af bf a b c | af bf a b -> c where haa :: af -> bf -> a -> b -> c -- Both are HLists instance (HList c, HAppend a b c) => HAA HTrue HTrue a b c where haa _ _ = hAppend instance HList a => HAA HTrue HFalse a b (HCons b a) where haa _ _ a b = HCons b a instance HList b => HAA HFalse HTrue a b (HCons a b) where haa _ _ a b = HCons a b -- deliberately unimplemented: at least one must be an HList... -- instance HList b => HAA HFalse HFalse a b c where test1 = hAppendArbitrary HNil True test2 = hAppendArbitrary True (HCons () HNil) test3 = hAppendArbitrary (HCons () HNil) (HCons False HNil) test4 = hAppendArbitrary (HCons () HNil) 'a' -- testf = hAppendArbitrary 'n' () -- TypeCast is skipped