[Haskell-cafe] some questions about type improvement, FDs vs TFs, and Hugs vs GHCi

[Claus Reinke]

consider

    class FD a b | a -> b
    instance CFD a b => FD a b

    class CFD a b
    instance CFD Bool Char

and the constraint 'CFD Bool c'.

logically, we know that if we have 'CFD Bool c', we also have 'FD Bool c',
which implies that 'c' is uniquely determined, which implies that 'c~Char'.

practically, the need to find an instance for 'CFD Bool c' does not
generate a demand for implied instances that could lead to this
improvement.

q1: should there be such a forward demand? ie, instead of 
    failing to find the instance for 'CFD Bool c', should the 
    transitive closure of forward implications be taken into
    account for FDs, similar to the transitive closure of
    backward implications? without such forward inferences,
    consistency of FDs seems hard to guarantee, unless one
    conservatively rules out everything that might lead to an
    inconsistency.

without such forward inference, implementations differ in their 
interpretation of this kind of code (as so often):

Hugs rejects the program ("Instance is more general than a 
dependency allows"), which is conservative, but seems to make
perfect sense: there's no FD for class 'CFD', so there's no
guarantee that all those implied instances of class 'FD' will
conform to its own FD.

that is easily fixed, it seems:

    class FD a b | a -> b
    instance CFD a b => FD a b

    class FD a b => CFD a b
    instance CFD Bool Char

now, there cannot be an instance of 'CFD' unless there also
is an instance of 'FD', in such a way that the parameters of
'CFD' obey the FD of 'FD'.

and, in fact, Hugs does now accept this code, and is able
to improve 'CFD Bool c' to 'CFD Bool Char', reducing
the latter as given:

    :t undefined :: CFD Bool c => c
    undefined :: Char

but wait a second: we have given an instance of 'CFD',
which according to the superclass constraint for that class,
is valid only if there is a corresponding instance of 'FD',
and there is such an instance of 'FD' if there is an instance
of 'CFD'. in other words: if the 'CFD' instance is accepted,
it is valid, if it isn't accepted, it is not valid.

q2: is this treatment of recursion for class instances intended,
    or is it an unexpected artifact of the special treatment of 
    superclass constraints?

GHCi also accepts this code, but it doesn't seem to do the
reduction or improvement:

     :t undefined :: CFD Bool c => c
    undefned :: CFD Bool c => c :: (CFD Bool c) => c

actually, GHCi accepts the first program, too! perhaps it
is delaying the FD consistency check until there is an
actual rather than a possible FD conflict? unfortunately
not, as we can see if we add a conflicting 'CFD' instance:

    class FD a b | a -> b
    instance CFD a b => FD a b
    
    class {- FD a b => -} CFD a b
    instance CFD Bool Char
    instance CFD Bool Bool

note that the conflict is not in 'CFD' but in the implied
instances of 'FD', which GHCi doesn't seem to take
into account for any FD consistency check:

    *Main> :t undefined :: CFD Bool c => c
    undefined :: CFD Bool c => c :: (CFD Bool c) => c
    *Main> :t undefined :: CFD Bool Char => c
    undefined :: CFD Bool Char => c :: c
    *Main> :t undefined :: FD Bool c => c
    undefined :: FD Bool c => c :: (CFD Bool c) => c
    *Main> :t undefined :: FD Bool Char => c
    undefined :: FD Bool Char => c :: c

only if we explicitly mention the inconsistent constraints
together, and directly in terms of 'FD', not just in terms of
'CFD', do we get the expected error, and even then, the
FD isn't used for improvement:

    *Main> :t undefined :: (CFD Bool Char,CFD Bool Bool) => c
    undefined :: (CFD Bool Char,CFD Bool Bool) => c :: c
    *Main> :t undefined :: (FD Bool Char,FD Bool Bool) => c
    
    <interactive>:1:0:
        Couldn't match expected type `Char' against inferred type `Bool'
        When using functional dependencies to combine
          FD Bool Bool,
            arising from the polymorphic type
                           `forall c. (FD Bool Char, FD Bool Bool) => c'
                         at <interactive>:1:0-44
          FD Bool Char,
            arising from the polymorphic type
                           `forall c. (FD Bool Char, FD Bool Bool) => c'
                         at <interactive>:1:0-44
    *Main> :t undefined :: (FD Bool Char,FD Bool c) => c
    undefined :: (FD Bool Char,FD Bool c) => c :: (CFD Bool c) => c

this looks like a bug to me, or am i missing something?

perhaps we fare better with TFs, as FD development in GHC
was put on hold while the new foundations for TFs were put
in place? unfortunately, we can't even define TFs in terms of 
classes, as has been discussed here before (in the context of 
using FD-based libaries in TF-based client code). what we'd 
like to write is something like:

    type family TF a
    type instance TF a = CTF a b => b -- won't work..
    
    class {- FD a b => -} CTF a b
    instance CTF Bool Char
    instance CTF Bool Bool

as with the FD-based variant, the definition of TF should not
work unless there is a functional relationship between the parameters
of 'CTF', but the 'TF' instance isn't even accepted syntactically
("Illegal polymorphic type in type instance").

q3: (a) are qualified types in type instances problematic, or
        just not yet implemented, or not yet investigated in theory?
    (b) what about the intended interaction of TFs and FDs in
        the example. it would seem to permit the use of FD-based
        code in TFs, as requested here earlier, but is this ever
        going to be supported?

questions, questions,.. does anybody have answers?-)
claus