Can I magic up type equality from a functional dependency?

Question

I'm trying to get some sense of MultiParamTypeClasses and FunctionalDependencies, and the following struck me as an obvious thing to try:

{-# LANGUAGE MultiParamTypeClasses
           , FunctionalDependencies
           , TypeOperators #-}

import Data.Type.Equality

class C a b | a -> b

fob :: (C a b, C a b') => proxy a -> b :~: b'
fob _ = Refl

Unfortunately, this doesn't work; GHC does not conclude b ~ b' from that context. Is there any way to make this work, or is the functional dependency not "internally" available?

Answer 1

I don't think this fact (as stated by the type of fob) is actually true. Due to the open world property of type classes, you can violate the fundep with module boundaries.

This is show by the following example. This code has only been tested with GHC 7.10.3 (fundeps were massively broken in older versions - don't know what happens then). Assume that you can indeed implement the following:

module A 
  (module A
  ,module Data.Type.Equality
  ,module Data.Proxy
  )where 

import Data.Type.Equality
import Data.Proxy 

class C a b | a -> b 

inj_C :: (C a b, C a b') => Proxy a -> b :~: b' 
inj_C = error "oops"

Then a few more modules:

module C where 
import A

instance C () Int 

testC :: C () b => Int :~: b 
testC = inj_C (Proxy :: Proxy ()) 

and

module B where 
import A

instance C () Bool 

testB :: C () b => b :~: Bool 
testB = inj_C (Proxy :: Proxy ()) 

and

module D where 

import A 
import B
import C 

oops :: Int :~: Bool
oops = testB

oops_again :: Int :~: Bool 
oops_again = testC 

Int :~: Bool is clearly not true, so by contradiction, inj_C cannot exist.

I believe you can still safely write inj_C with unsafeCoerce if you don't export the class C from the module where it's defined. I've used this technique, and have extensively tried, and not been able to write a contradiction. Not to say it's impossible, but at least very difficult and a rare edge case.