Thanks for the reply. I don't quite understand why guessing whether there is an intermediate type would be so magical, though. Let's simplify: data A data B class IsNotFirst a class IsAfter b a instance (IsAfter b a) => IsNotFirst a instance IsAfter B A Here we've separated out the ambiguous type issue from the unification. Note that *already*, if I query with undefined::(IsNotFirst A => a), I get: No instance for (IsAfter b A) arising from a use of ‘t’ The type variable ‘b’ is ambiguous Note: there is a potential instance available: instance [overlap ok] IsAfter B A Generally, GHC is doing the work that I wanted it to *in the error message*. In what sense, then, is this impossible? And why is there some inexcusable use of CWA here? Instances already have (if you squint) a negation-as-failure semantics. "instance (IsAfter b a) => IsNotFirst a" doesn't *in that sense* look that different to me than "instance (IsSecond a) => IsNotFirst a": adding extra instance declarations can 'change the truth-value' of the right-hand side. Thanks again, Julian On Thu, Jun 26, 2014 at 1:58 AM, Andras Slemmer <0slemi0@gmail.com> wrote:
Think about what you're asking from the compiler. If it sees a (Path a c) constraint it would have to magically guess whether there is an intermediate type b for which (Path a b) and (Path b c), which is impossible.
Logic programming relies on the closed world assumption, meaning that if a statement cannot be proven within the closed world we are working in then it is false. Haskell typeclasses don't work like this; there is no closed world of types, so the compiler cannot "refute" a constraint.
In prolog you'd have something like this: path(A,C) :- path(A,B), path(B,C). (havent used prolog for a while so syntax might be off)
If you translate this to first order logic you'd have: \forall A,C.(path(A,C) <- \exists B.(path(A,B)^path(B,C)))
It is the existential that is emulated with the cwa and cannot be emulated in haskell's typesystem.