<div dir="ltr">Consider the following program:<div><br></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px"><div><div>{-# LANGUAGE TypeFamilyDependencies #-}</div></div><div><div><br></div></div><div><div>data D x</div></div><div><div><br></div></div><div><div>type family F t = s | s -> t</div></div><div><div>type instance F (D t) = D (F t)</div></div><div><div><br></div></div><div><div>f :: F s -> ()</div></div><div><div>f _ = ()</div></div><div><div><br></div></div><div><div>g :: D (F t) -> ()</div></div><div><div>g x = f x</div></div><div><div><br></div></div><div><div>main = return ()</div></div></blockquote><div><br></div><div>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><br></div><div>1. "F s ~ D (F t)" (from function call)</div><div>2. "D (F t) ~ F (D t)" (from the right hand side of the injective type definition)</div><div><br></div><div>Therefore we should be able to derive:</div><div><br></div><div>3. "F s ~ F (D t)" (type equality is transitive)</div><div>4. "s ~ D t" (as F is injective)</div><div><br></div><div>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><br></div><div>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">https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/injective-type-families-acm.pdf</a> section 5.1 p125):</div><div><br></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> </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> </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> </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><br></div><div>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>