[Haskell] TryTypeCast hackery possible?

[Andreas Schropp]

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).