<div dir="ltr"><br><div>> <span style="color:rgb(0,0,0);white-space:pre-wrap">On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers </span><span style="color:rgb(0,0,0);white-space:pre-wrap">wrote:</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">> </span><span style="color:rgb(0,0,0);white-space:pre-wrap">Maybe our Haskell'17 paper about Elaboration on Functional Dependencies </span><span style="color:rgb(0,0,0);white-space:pre-wrap">sheds some more light on your problem:</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">Thanks Tom, I've also been working through the 2011 expanded version of '</span>System F with Type Equality Coercions<span style="color:rgb(0,0,0);white-space:pre-wrap">' that Adam suggested.</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">I'm finding your 2017 paper's proposals not up to the job, because it doesn't consider FunDeps for Overlapping Instances; and unnecessary because the examples it's addressing can be fixed purely using FunDeps, with their semantics per the 2006 'via CHRs' paper. The chief problems with using FunDeps in GHC code is GHC doesn't follow that semantics; neither does it follow any other well-principled/documented semantics.You can get it to accept a bunch of instances then find that taken together they're not consistent and confluent, in the sense of the 'via CHRs' paper.</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">Specifically, re the 2017's paper Challenge 1: Enforcing (essentially Trac #10675). That set of instances in the example is not valid by the 'via CHRs' rules, and should be rejected. Hugs indeed rejects that code. GHC accepts it and #10675 shows what sort of incoherence can result. I'm not seeing we need to translate to Type Families/System FC to explain it.</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap">Re Challenge 2: Elaborating (which is Trac #9627 that gives the main example for the paper). We can fix that code with an extra `~` constraint:</span></div><div><span style="color:rgb(0,0,0);white-space:pre-wrap"><br></span></div><div><pre class="gmail-code gmail-highlight" lang="plaintext"><span id="gmail-LC1" class="gmail-line" lang="plaintext">    class C a b | a -> b</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span id="gmail-LC2" class="gmail-line" lang="plaintext">    instance C Int Bool</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext"><br></span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span id="gmail-LC4" class="gmail-line" lang="plaintext">    f :: (C Int b, b ~ Bool) => b -> Bool</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span id="gmail-LC5" class="gmail-line" lang="plaintext">    f x  = x  </span>
</pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext">(Or in Hugs with a `TypeCast` instead of the `~`.)</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext"><br></span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext">Is that extra constraint onerous? The signature already has `Bool` hard-coded as the return type, so I don't see it's any more onerous.</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext">Or put that signature as</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext">    f :: (C Int b) => b -> b</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext">Which also has the effect `b` must be `Bool`.</span></pre><pre class="gmail-code gmail-highlight" lang="plaintext"><span class="gmail-line" lang="plaintext"><br></span></pre><pre class="gmail-code gmail-highlight" lang="plaintext">I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity.</pre><pre class="gmail-code gmail-highlight" lang="plaintext"><br></pre><pre class="gmail-code gmail-highlight" lang="plaintext">AntC</pre></div></div>