Your second example shouldn't (and doesn't) compile, as the IsNotFirst instance has an ambiguous variable 'b'. What you want is this 'b' to be existentially quantified and have the compiler provide a witness for it.

Again, Haskell doesn't have a closed world of types. Even if the compiler doesn't find a 'b' in say the current module it cannot refute an IsNotFirst constraint, as an IsAfter instance may be defined in another module.

module A where

weirdId :: IsNotFirst a => a -> a

weirdId = id

Should this compile if we don't have an IsAfter instance in the current module? What if we define one in module B which imports module A? What if we have two IsAfter instances? Which instance should it use?

> adding extra instance declarations can 'change the truth-value' of the right-hand side.

No, they cannot. instance (IsSecond a) => IsNotFirst a translates to (\forall a. IsSecond(a) -> IsNotFirst(a)), which will always hold. (Unless you switch on overlappinginstances which you shouldnt)

On 25 June 2014 23:06, Julian Arni <jkarni@gmail.com> wrote:

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.