> On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote:

> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:

Thanks Tom, I've also been working through the 2011 expanded version of 'System F with Type Equality Coercions' that Adam suggested.

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.

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.

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:

    class C a b | a -> b

    instance C Int Bool

    f :: (C Int b, b ~ Bool) => b -> Bool

    f x  = x

(Or in Hugs with a `TypeCast` instead of the `~`.)

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.

Or put that signature as

    f :: (C Int b) => b -> b

Which also has the effect `b` must be `Bool`.

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.

AntC