On the FD impasse:
Witness.hs:33:0: Couldn't match expected type `m'' (a rigid variable) against inferred type `RealWitness a a'' `m'' is bound by the type signature for `>>' at Witness.hs:11:29 When using functional dependencies to combine Witness WitnessReally a b (RealWitness a b), (and a screenful more) Any suggestions?
What follows isn't so much a suggestion, but I think it's a description of this error's origins. Note that >>='s signature from the class declaration
class Witness w a b m | w a b -> m, m -> w a b where (>>=) :: (Witness w a a' m', Witness w a' b m'') => m' x -> (x -> m'' y) -> m y (>>) :: (Witness w a a' m', Witness w a' b m'') => m' x -> m'' y -> m y f >> g = f >>= const g private_return :: x -> m x fail :: String -> m x
is "copied" to this instance declaration,
instance Witness WitnessReally a b (RealWitness a b) where
so we have: (>>=) :: ( Witness WitnessReally a a' m' , Witness WitnessReally a' b m'' ) => m' x -> (x -> m'' y) -> (RealWitness a b) y Now consider what the signature of >>= for this instance would be if this "copy from the class to the instance" operation were savvy to our plans: (>>=) :: ( Witness WitnessReally a a' (RealWitness a a') , Witness WitnessReally a' b (RealWitness a' b) ) => (RealWitness a a') x -> (x -> (RealWitness a' b) y) -> (RealWitness a b) y This signature is what the FD analyzer determines. Our above error arises because the actual signature of >>= has m' where the FDs indicate we'll always have (RealWitness a a'). Does that seem accurate? (I've put off actually looking at the GHC source for ages now...) In my opinion, this is reminiscent of some of the scoped-type variable issues and notions (e.g. wobbly types). By the functional dependency |w a b -> m|, we know that the m' and m'' in the signature of >>= will be determined as some particular types (i.e. the class is a type function from w a b to m), and we'd just like to refer to whatever those types actually are as m' and m''. It seems the FD analyzer determines for us what those particular types are, but then the type-checker is unhappy that we're naming them m' and m'' when we should know more about them (e.g. that they have a RealWitness tycon). Unfortunately, we have no choice about the signature of >>= at the instance declaration, since it's copied straight from the class declaration. If m' and m'' were recognized as partially wobbly variables, then maybe this wouldn't be a problem. Or maybe wobbly types could be framed in terms of functional dependencies on a non-method's signature? (The rest might be off-topic.) This situation also conjures up some of my own confusion about FDs, the open world assumption, and "finalizing" a typeclass. One of my main confusions with FDs is how they play with the open world assumption. Another confusion is that just because your instance declarations satisfy the FDs of a class, they won't necessisarily allow the type inference engine to act in accord to those FDs. Sometimes you have to break a class's definition into ancillary classes, each with one of the FDs you want and appropriate instance declarations to drive the inference along those particular FDs. If you try to cram all of the FDs into one set of instance declarations, they tend to choke the FD analyzer. (I read FDs as "a b and c" determine "x y and z"; this is a description of the class's membership, but the FD analysis takes place on the instance declarations themselves and not necessarily the types admitted to the class.) Nick _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe