Interesting example | class Monad2 m a ma | m a -> ma, ma -> m a where | return2 :: a -> ma | bind2 :: Monad2 m b mb => ma -> (a -> mb) -> mb | _unused :: m a -> () | _unused = \_ -> ()
| instance Monad2 [] a [a] where | bind2 = error "urk" The functional dependencies say m a -> ma Instantiating this with the instance declaration instance Monad2 [] a [a] we can deduce that given any constraint (Monad2 t1 t2 t3), if t1 = [], then t3 must be [t2] In the instance declaration, we instantiate the type of bind2 to get the type of bind2 needed for this particular instance declaration: bind2 :: forall b mb. Monad2 [] b mb => ma -> (a -> mb) -> mb Now the rule above says "that means mb must be [b]" and that gives rise to the error. GHC is consistent about this --- if you don't supply an defn for bind2, it makes one up, and complains in more or less the same way. Here's a less complicated variant of the same problem: class C a b | a -> b where {} instance C Int Int where {} f :: (C Int b) => Int -> b f x = x Is the defn of f legal? Both GHC and Hugs reject it because the inferred type of f is more like C Int Int => Int -> Int Functional dependencies tell us that 'b' must be Int, so in fact the two types are equivalent. In this example the programmer could write the 'correct' type, but in your case you can't because the type signature arises by instantiating the one in the class declaration. I'm really not sure what to do about this. GHC has an excellent way of keeping me honest in type-checking: the type checker has to produce a translation of the program into the (typed) core language. What could f's translation look like. It must presumably be f (d::C Int Int) (x::Int) = x giving f the type f :: C Int Int -> Int -> Int Another translation could be f b (d::C Int b) (x::Int) = x (the 'b' is a type variable, a big-lambda binding) giving f the type f :: forall b. C Int b -> Int -> Int But what I *cannot* get is the type f : forall b. C Int b -> Int -> b how could I write the term? f b (d:: C Int b) (x::Int) = ????? I suppose I could use (unsafeCoerce x) as the RHS, which amounts to saying "in every call to f, b will be Int, so we know that the coercion is safe". But that is a scarily global property. For example, if a call site of f does not "see" the instance declaration, it might call f with an argument of type (C Int Bool) or something. Nor can I see an easy way to insert the 'right' coercions in general. Bottom line: excellent point, but I can't see how to fix it. Maybe there are some fundep experts out there who can guide us through the swamp? Simon _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell