Is it time to start deprecating FunDeps?

[AntC]

> AntC <anthony_clayden at ...> writes:
> 
> > <oleg <at> ...> writes:
> > 
> > I think this mechanical way is not complete.
> 

On further thought/experiment, I rather think it is -- for one of your 
counter examples.

Firstly, I apologise to Oleg. I had mis-remembered his solution to the 
class Sum example ...
> 
> > 
> >         class Sum x y z | x y -> z, x z -> y
> > 
>  your own solution has a bunch of helper classes (each with one-
> directional FunDeps).

This Sum is actually a helper called Sum2 in the PeanoArithm module. 
Here's Oleg's full code (modulo alpha renaming):
{-
    class Sum2 a b c | a b -> c, a c -> b
    instance Sum2 Z b b
    instance (Sum2 a' b c') => Sum2 (S a') b (S c')

    -- note that in the FunDeps, var a is not a target
    -- so the instances discriminate on var a
-}

And I must apologise to myself for doubting the mechanical translation in 
face of cyclical FunDeps. Here it is:

    class Sum2 a b c         -- | a b -> c, a c -> b
    instance (b ~ c) => Sum2 Z b c
    instance (c ~ (S c'), Sum2 a' b c') => Sum2 (S a') b c


> Your [Oleg's] solution has a single instance declared for the 
> Sum class, with three bare typevars. So it is valid by step 1. of the 
> rules I gave. (In your solution all the 'hard work' is done by the 
> helpers, which are constraints on that single instance.)
> 

That much I had remembered correctly. So I don't need to change the Sum 
class (except to remove the FunDep):

    class Sum a b c          -- | a b -> c, a c -> b, b c -> a
    instance (Sum2 a b c, Sum2 b a c) => Sum a b c

The tests from Oleg's code (ta1, ta2) infer the same types. Test ta3 fails 
to compile -- as it does for Oleg.

(My code does need UndecidableInstances, as does Oleg's.)