<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">Your original example looks like a new bug to me. #10833 is about givens (that is, a context that would be specified in a function type signature), and I don't think that's at issue here.</div><div class=""><br class=""></div><div class="">I agree with you that your program should be accepted.</div><div class=""><br class=""></div><div class="">Might you post a ticket?</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Richard</div><br class=""><div><blockquote type="cite" class=""><div class="">On Oct 28, 2016, at 10:30 PM, Clinton Mead <<a href="mailto:clintonmead@gmail.com" class="">clintonmead@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Sorry for talking to myself, but I think the answer to my question is here:<br class=""><br class=""><a href="https://ghc.haskell.org/trac/ghc/ticket/10833" class="">https://ghc.haskell.org/trac/ghc/ticket/10833</a><br class=""></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Sat, Oct 29, 2016 at 12:26 PM, Clinton Mead <span dir="ltr" class=""><<a href="mailto:clintonmead@gmail.com" target="_blank" class="">clintonmead@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="">Also is there a type-checker plugin that helps with this? If not, would it be possible to write one, or was there some intentional reason why this inference was not included?</div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br class=""><div class="gmail_quote">On Sat, Oct 29, 2016 at 11:54 AM, Clinton Mead <span dir="ltr" class=""><<a href="mailto:clintonmead@gmail.com" target="_blank" class="">clintonmead@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="">Consider the following program:<div class=""><br class=""></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px" class=""><div class=""><div class="">{-# LANGUAGE TypeFamilyDependencies #-}</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">data D x</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">type family F t = s | s -> t</div></div><div class=""><div class="">type instance F (D t) = D (F t)</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">f :: F s -> ()</div></div><div class=""><div class="">f _ = ()</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">g :: D (F t) -> ()</div></div><div class=""><div class="">g x = f x</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">main = return ()</div></div></blockquote><div class=""><br class=""></div><div class="">The problem seems to be the call from "g" to "f". We're calling "f" with an argument of type "D (F t)". "f" then has to determine what "s" is in it's signature. We know: </div><div class=""><br class=""></div><div class="">1. "F s ~ D (F t)" (from function call)</div><div class="">2. "D (F t) ~ F (D t)" (from the right hand side of the injective type definition)</div><div class=""><br class=""></div><div class="">Therefore we should be able to derive:</div><div class=""><br class=""></div><div class="">3. "F s ~ F (D t)" (type equality is transitive)</div><div class="">4. "s ~ D t" (as F is injective)</div><div class=""><br class=""></div><div class="">I suspect the part we're missing in GHC is step 4. I recall reading this somewhere but I can't find where now.</div><div class=""><br class=""></div><div class="">However, the paper about injective types says that this style of inference, namely "F a ~ F b => a ~ b" should occur. I quote (<a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/injective-type-families-acm.pdf" target="_blank" class="">https://www.microsoft.com/en-<wbr class="">us/research/wp-content/uploads<wbr class="">/2016/07/injective-type-<wbr class="">families-acm.pdf</a> section 5.1 p125):</div><div class=""><br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">So, faced with the constraint F α ∼ F β, the inference engine

does not in general unify α := β; so the constraint F α ∼ F β is

not solved, and hence f (g 3) will be rejected. But if we knew that

F was injective, we can unify α := β without guessing. </blockquote><div class=""> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Improvement (a term due to Mark Jones (Jones 1995, 2000)) is a

process that adds extra "derived" equality constraints that may make

some extra unifications apparent, thus allowing inference to proceed

further without having to make guesses. In the case of an injective

F, improvement adds α ∼ β, which the constraint solver can solve

by unification. In general, improvement of wanted constraint is

extremely simple:

</blockquote><div class=""> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Definition 11 (Wanted improvement). Given the wanted constraint

F σ ∼ F τ , add the derived wanted constraint σn ∼ τn for each

n-injective argument of F.

</blockquote><div class=""> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Why is this OK? Because if it is possible to prove the original

constraint F σ ∼ F τ , then (by Definition 1) we will also have a

proof of σn ∼ τn. So adding σn ∼ τn as a new wanted constraint

does not constrain the solution space. Why is it beneficial? Because,

as we have seen, it may expose additional guess-free unification

opportunities that that solver can exploit.</blockquote><div class=""><br class=""></div><div class="">Am I correct in my assessment of what is happening here with GHC? Is there anyway to get it to compile this program, perhaps with an extension? </div></div>

</blockquote></div><br class=""></div>

</div></div></blockquote></div><br class=""></div>

_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></body></html>