<div dir="ltr"><div><div>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.<br>
<br>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.<br>
<br></div><div>module A where<br></div><div>weirdId :: IsNotFirst a => a -> a<br></div><div>weirdId = id<br><br></div><div>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?<br>
</div><br>> adding extra instance declarations can 'change the truth-value' of the right-hand side. <br><br></div>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)<br>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On 25 June 2014 23:06, Julian Arni <span dir="ltr"><<a href="mailto:jkarni@gmail.com" target="_blank">jkarni@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">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:<div><br></div><div>data A</div><div>data B</div><div><div>

class IsNotFirst a</div><div>class IsAfter b a</div><div>instance (IsAfter b a) => IsNotFirst a</div><div>instance IsAfter B A</div></div><div><br></div><div><br></div><div>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:</div>

<div><br></div><div><div>  No instance for (IsAfter b A) arising from a use of ‘t’</div><div>    The type variable ‘b’ is ambiguous</div><div>    Note: there is a potential instance available:</div><div>      instance [overlap ok] IsAfter B A</div>

</div><div><br></div><div>Generally, GHC is doing the work that I wanted it to *in the error message*. In what sense, then, is this impossible?</div><div>  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. </div>

<div><br></div><div><br></div><div>Thanks again,</div><div>   Julian</div><div class=""><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Jun 26, 2014 at 1:58 AM, Andras Slemmer <span dir="ltr"><<a href="mailto:0slemi0@gmail.com" target="_blank">0slemi0@gmail.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div><div>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.<br>


</div><br>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.<br>


<br></div>In prolog you'd have something like this:<br></div>path(A,C) :- path(A,B), path(B,C).<br></div>(havent used prolog for a while so syntax might be off)<br><br></div>If you translate this to first order logic you'd have:<br>


</div>\forall A,C.(path(A,C) <- \exists B.(path(A,B)^path(B,C)))<br><br></div>It is the existential that is emulated with the cwa and cannot be emulated in haskell's typesystem.<br></div><div><div>
<div class="gmail_extra"><br>
<br><div class="gmail_quote"><br></div></div></div></div></blockquote></div></div></div></div>
</blockquote></div><br></div>