[Haskell-cafe] Re: help with MPTC for type proofs?

[David Roundy]

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