More thoughts on #15632: towards a theory of overlaps+FunDeps about ghc-proposals

[AntC2]

I'm thinking rule B) i) is not needed:

i) The FunDep is full;

We do require both ii) and iii)

ii) One of the instances is strictly more specific; and

iii) That instance's argument positions taken together are strictly more specific.

That means that if the FunDep is non-full, the 'extraneous' positions of the more specific instance must be not less specific. In which 'extraneous' means the positions not mentioned in the FunDep. Then this rule still rejects Trac #10675 example. (Those instances are apart/in no substitution ordering, taking the extraneous positions into account.)

Note there might be several FunDeps (particularly if we allow for non-full); then the more specific instance must have its argument positions (taken together) more specific for each FunDep.

Hmm this still allows

class D x a b  | a -> b, b -> a

instance D [x] Int Bool
instance (a ~ Int, b ~ Char) => D x a b

Hugs rejects those instances (using TypeCast instead of ~.) GHC 8.6.4 accepts them. But this might be one of the (many) cases where GHC seemingly accepts instances, then you find they're unusable.

(The extraneous x here is inessential: GHC accepts those instances without it, or if both instances have [x].)

The Hugs (with my modification) rejection is Constraints are not consistent with functional dependency, note the Constraints. That means Hugs/my mod has initially accepted the instance heads, then applied the improvements from Constraints, then uncovered an inconsistency.

[AntC2]

I still hanker after writing my instances like this:

-- type-level predicate: is this a function?
class IsFunc a p  | a -> p

instance IsFunc (a1 -> a2) True
instance IsFunc a          False

That is, putting the result type directly without a catch-all more general instance head and the distracting improvements. Then the rules might be (and still allowing for non-full FunDeps, I'll keep the same numbering as for B).) Reminder of context: this check applies, for each FunDep, when comparing instance heads pairwise:

D) Relax further to no consistency check on the FunDep target, providing all of:

ii) one instance is strictly more specific, ignoring the FunDep target (explained below); and

iii) That instance's argument positions taken together are strictly more specific.

Re "ignoring the FunDep" target, we need to still include extraneous positions in the comparison. For class D instances from the previous comment we in effect

• for FunDep a -> b compare D [x] Int ... vs D x a ....

• for FunDep b -> a compare D [x] ... Bool vs D x ... b.

The rule doesn't say to ignore all FunDep targets holus bolus. That is, don't compare D [x] ... ... vs D x ... ....

There's a gotcha I'm still thinking about: whichever instance is more specific at ii), it must be the same instance across all FunDeps. That's why B) ii) is straightforward to check. Not sure if I can construct a counter-example -- if not, need to figure out why.

[AntC2]

whichever instance is more specific at ii), it must be the same instance across all FunDeps.

I'm thinking: if the improvements via FunDeps are non-consistent between different instances, there must be no opportunity for selecting different instances (different improvements) for the same Wanted constraint. And the way to ensure that is that one instance is more specific no matter which FunDep target gets ignored.

So this should be rejected

instance D  x  (Just Int) b       --  x  less specific, (Just Int) more, b    less
instance D [x] (Just a  ) Bool    -- [x] more specific, (Just a  ) less, Bool more

The obvious counter-example (not to reject) is

instance (b ~ Bool) => D [x] Int b
instance (a ~ Int ) => D [x] a   Bool

Neither instance is more specific; the FunDep a -> b check will ignore b and Bool, and think the bare a head is less specific; the FunDep b -> a check will ignore a and Int, and think the bare b head is less specific.

This is where we run foul of the diamond inheritance pattern. I want to say those two instances implement (and are consistent with)

instance D [x] Int Bool

That is more specific than either, and the mgu of the two, so I want to count as overall coherent overlap. (But GHC wants them both to be flagged {-# INCOHERENT #-}; and Hugs rejects them.)

[AntC2]

And the way to ensure that is that one instance is more specific no matter which FunDep target gets ignored.

Even considering only one FunDep, the target of the more specific instance can't be less specific; it can be apart. So these not allowed

class C a b  | a -> b
instance C (Just a1) a1
instance C a         Char

Because there's a danger Wanted C alpha Char will match to the second instance, without trying harder to improve alpha ~ (Just a1).