Problem with functional dependencies

[Chris Kuklewicz]

I have a guess...

Daniel Gorín wrote:
> Hi
> 
> I have some code that uses MPTC + FDs + flexible and undecidable
> instances that was working fine until I did a trivial modification on
> another part of the project. Now, GHC is complaining with a very
> confusing (for me, at least) error message. I've been finally able to
> reproduce the problem using these three small modules:
> 
>> {-# LANGUAGE MultiParamTypeClasses #-}
>> {-# LANGUAGE FunctionalDependencies #-}
>> {-# LANGUAGE FlexibleInstances #-}
>> module M1
>>
>> where
>>
>> data M n = M
>> data F n = F
>>
>> class C m f n | m -> n, f -> n where
>>     c :: m -> f -> Bool

The "m->n" functional dependency means that I tell you
"C x _ z" is an instance then you whenever you match "x" that you
must have the corresponding "z".

>>
>> instance C (M n) (F n) n where
>>     c _ _ = True

This promises that "C x _ z" with x=="M n" has z==n

> 
>> {-# LANGUAGE MultiParamTypeClasses #-}
>> {-# LANGUAGE UndecidableInstances #-}
>> {-# LANGUAGE FlexibleInstances #-}
>> module M2
>>
>> where
>>
>> import M1
>>
>> newtype F'= F' (F N)
>>
>> data N = N
>>
>> instance C m (F N) N => C m F' N where
>>      c m (F' f) = c m f

By the "m->n" functional dependency, the above implies that _any_ "m" must map
to the type M2.N:  "m -> M2.N"

This kills you in M3...

> 
>> module M3
>>
>> where
>>
>> import M1
>> import M2()
>>
>> data N' = N'
>>
>> go :: M N' -> F N' -> Bool
>> go m f = c m f

(M N') matches "m" so the type "z" of "C x y z" must be M2.N

That (M N') also works with the first instance is irrelevant. You have given
conflicting instances, and GHC _cannot_ satisfy the the contradicting functional
dependencies you have declared.

GHC gives a poor error message, but errors with that many LANGUAGE flags do
become more opaque.

> 
> Now, when trying to compile M3 (both in 6.6.1 and 6.8.1) I get:
> 
> M3.hs:11:0:
>     Couldn't match expected type `N'' against inferred type `M2.N'
>     When using functional dependencies to combine
>       C m M2.F' M2.N, arising from the instance declaration at M2.hs:13:0
>       C (M N') (F N') N', arising from use of `c' at M3.hs:11:9-13
>     When generalising the type(s) for `go'
> 
> It is worth observing that:
> 
> - M2 compiles fine
> - No type defined in M2 is visible in M3
> - if the "import M2()" is commented out from M3, it compiles fine
> - if, in M3, N' is placed by N (needs to be imported), everything
> compiles again
> 
> Normally, it takes me some time to digest GHC's type-classes-related
> error messages, but after some reflection, I  finally agree with them.
> This time, however, I'm totally lost. I can't see any reason why N' and
> M2.N would have to be unified, nor why this code should be rejected.
> 
> Any help would be much appreciated!
> 
> Daniel
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users