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
instance C (M n) (F n) n where c _ _ = True
{-# 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
module M3
where
import M1 import M2()
data N' = N'
go :: M N' -> F N' -> Bool go m f = c m f
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
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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Hi, Chris Thanks for your answer. I guess that my intuitions of what functional dependencies and context meant were not very accurate (see below)
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".
That's what I thought..
instance C (M n) (F n) n where c _ _ = True
This promises that "C x _ z" with x=="M n" has z==n
I agree....
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...
Here I was expecting the context "C m (F N) N" to work as a logical guard, something like: 'for all m such that "C m (F N) N" holds, "C m F' N" must hold too' and since '"C m (F N) N" holds' would already imply 'm -> N', then "C m F' N" would not produce any contradiction. I guess this view doesn't hold when FlexibleInstances is on.... Anyway, it makes (kind of) sense now...
By the way, if you make the class C fundep declaration into:
class C m f n | m f -> n where
then it compiles. This means ((M n) and (F n) imply N) and ("any m" and F' imply N') which no longer conflict.
Thanks again for the tip, I will try it out! Daniel
By the way, if you make the class C fundep declaration into:
class C m f n | m f -> n where
then it compiles. This means ((M n) and (F n) imply N) and ("any m" and F' imply N') which no longer conflict. 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
instance C (M n) (F n) n where c _ _ = True
participants (2)
-
Chris Kuklewicz -
Daniel Gorín