Can someone explain to me why this doesn't work? > {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-} > module MPTC where > > class C a b c d | a b c -> d, a d c -> b > > instance (C a b c d) => C a d c b > > data P a b = P deriving (Show) > > data CommuteResult a b c where > CR :: C a b c d => (P a d, P d c) -> CommuteResult a b c > > commute :: (P a b, P b c) -> CommuteResult a b c > commute (P, P) = CR (P, P) > > test (x,y) = do CR (y',x') <- return $ commute (x,y) > CR (y'', x'') <- return $ commute (x,y) > CR (x''',y''') <- return $ commute (y',x'') > return ()
By my logic, it seems that if x :: P a b y :: P b c then y' and x'' must have types y' :: C a b c d => P a d x'' :: C a b c e => P e c but the functional dependencies of C tell us that e and d must be the same type, so the code should typecheck (which it doesn't)! I'm thinking that either the functional dependency constraint is weaker than I thought, or that somehow GADTs aren't interacting with FDs as I'd like, but I'm not sure which. Or, of course, it may be that my recursive instance is not doing what I like. Or I may be just plain confused, as is pretty clearly the case... -- David Roundy http://www.darcs.net _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe