Equality constraints (~): type-theory behind them

[Anthony Clayden]

> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20190326/adff21d2/attachment.html>