Problem with functional dependencies
Chris Kuklewicz
haskell at list.mightyreason.com
Fri Nov 16 18:26:41 EST 2007
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
More information about the Glasgow-haskell-users
mailing list