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