While reading on Oleg's typeclass-overloaded functions via "local" (*) backtracking (http://okmij.org/ftp/Haskell/poly2.txt), it occured to me that in order to support true Prolog-style instance/clause selection (Oleg seems to only use guards not based on unification-success), one would need TryTypeCast (mixture of TypeCast and TypeEq from HList paper: unify if possible and return HTrue, otherwise return HFalse). After a bit of experimentation my best try is this: -- should i somehow express the "local" functional dependencies -- res=HTrue a -> b and res=HTrue b -> a? class TryTypeCast a b res | a b -> res -- pretending polymorphism in t to prevent early unification of a and b, -- as seen in HLIST paper class TryTypeCast' t a b res | t a b -> res class TryTypeCast'' t a b res | t a b -> res instance TryTypeCast' () a b res => TryTypeCast a b res instance TryTypeCast'' t a b res => TryTypeCast' t a b res instance TryTypeCast'' () a a HTrue instance TypeCast HFalse res => TryTypeCast'' () a b res But it doesnt work (of course? is there even a workaround?) in the interesting cases, as unresolved overlapping gets into my way. (*) it seems that in the current model only "tail-recursive", in the search path sense, only needing local choice between success or search-deepening (the traditional append/3 would be tail-recursive in this way; not sure if this is standard terminology), predicates are possible. How to extend on that? I thought about a history of clause/instance selections per "predicate", hacking up Oleg's GFN-Interpreter in that regard, or even employing type-level CPS, based on the notion of closures in Oleg's Computable Types I (http://www.haskell.org/pipermail/haskell/2006-September/018486.html).