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.