<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Mon, May 7, 2018 at 10:27 PM, Li-yao Xia <span dir="ltr"><<a href="mailto:lysxia@gmail.com" target="_blank">lysxia@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Clinton,<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
instance A t => C' t Satisfied tb where<br>
   ...<br>
<br>
instance B t => C' t ta Satisfied where<br>
   ...<br>
<br>
instance (A t, B t) => C' t Satisfied Satisfied where<br>
   ...<br>
<br>
</blockquote>
<br></span>
The first two instances will only be picked if `ta` or `tb` can be determined to not "unify" with `Satisfied`. But a type family that cannot reduce will still "unify" with anything (it might just be that the rules to reduce it exist but are not in scope).<br>
<br></blockquote><div>Why is this the case? Can't the first instance be picked even if tb hasn't been determined not to unify with "Satisfied", as long as the 2nd type variable does unify with "Satisfied"?</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'm not sure "unify" is the right term when talking about this behavior of type families, but it's the one used in describing the instance resolution algorithm ("find all instances that unify with the target constraint"): <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instances" rel="noreferrer" target="_blank">https://downloads.haskell.org/<wbr>~ghc/latest/docs/html/users_gu<wbr>ide/glasgow_exts.html#overlapp<wbr>ing-instances</a><br>
<br>
These instances are only useful if we can actually decide satisfiability of constraints, which contradicts the open-world assumption as you mentioned.<span class=""><br>
<br>
<br>
IsSatisfiable c = Satisfied -- (if c is satisfiable)<br></span>
IsSatisfiable c = Unsatisfiable -- (if c is not satisfiable)<br>
<br></blockquote><div>But your example is different to mine. I've said I'm looking for the following:</div><div><br></div><div>

<div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial"><font face="monospace, monospace">IsSatisfiable c = Satisfied -- (if c is satisfiable)</font></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial"><div style="color:rgb(34,34,34);font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><font face="monospace, monospace" style="">IsSatisfiable c =<span style="font-weight:400"> </span><span style="color:rgb(34,34,34);font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><b>IsSatisfiable c</b></span><span style="font-weight:400"> </span>-- (if c is not satisfiable)</font></div></div>

<br></div><div>Notice I never mentioned "Unsatisfiable". Without "Unsatisfiable", I don't see how this violates the open-world assumption. </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Regards,<br>
Li-yao<div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/haskell-caf<wbr>e</a><br>
Only members subscribed via the mailman list are allowed to post.</div></div></blockquote></div><br></div></div>