the MPTC Dilemma (please solve)

[Claus Reinke]

[I suggest to keep follow-on discussions to the haskell prime list,
 to avoid further copies]

> continuing the list of odd cases in type class handling, here is a
> small example where overlap resolution is not taken into account
> when looking at FDs. 

actually, one needs to take both into account to arrive at the 
interpretation I favour:

- variables in the range of an FD can never influence instance
    selection if the variables in the domain of that FD are given
    (for, if they did, there'd be two instances with different range
    types for the same domain types -> FD violation)

- in other words, FDs not only tell us that some type relations
    are functional, they can be seen as roughly similar to what is 
    called mode declarations in logic programming: they tell us 
    with which input/output combinations a type relation may 
    be used

- for each FD a given constraint is subject to, the range types 
    should be ignored during instance selection: the domain types
    of the FD constitute the inputs and are sufficient to compute 
    unique FD range types as outputs of the type relation. the
    computed range types may then be compared with the range 
    types given in the original constraint to determine whether the
    constraint can be fulfilled or not

if we apply these ideas to the example I gave, instance resolution
for the "3 parameter, with FD"-version proceeds exactly as it
would for the "2 parameter"-version, using best-fit overlap
resolution to determine a unique 3rd parameter (range of FD)
from the first two (domain of FD).

this would seem similar to what we do at the function level:

    f a b | let res = True, a==b = res
    f a b | let res = False, otherwise = res

here, the implementation does not complain that f isn't functional
because we could instantiate {a=1,b=1,res=False} as well as 
{a=1,b=1,res=True} - instead it treats res as output only, a and b 
as input, and lets first-fit pattern matching resolve the overlap in 
the patterns. these rules describe a function because we say it does.

whereas, at the type class level, the implementations say "okay,
you said this is a type function, with two input and one output 
parameters, but if I ignore that for the moment, then overlap 
resolution doesn't kick in because of the different 3rd input 
parameter, and now there are two instances where there should 
only be one {TEQ a a T, TEQ a a F}; and if I now recall
that this should be a type function, I have to shout 'foul!'".

am I the only one who thinks this does not makes sense?-)

cheers,
claus
 
>    {- both ghc and hugs accept without 3rd par and FD
>       neither accepts with 3rd par and FD -}
> 
>    data T = T deriving Show
>    data F = F deriving Show
> 
>    class    TEQ a b {- tBool | a b -> tBool -} where teq :: a -> b -> Bool
>    instance TEQ a a {- T                    -} where teq _ _ = True
>    instance TEQ a b {- F                    -} where teq _ _ = False
> 
>    test = print (teq True 'c', teq True False)