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?

Vehemence

If you encode the fundep as class (F a ~ b) => C a b where type F a as described in the GHC docs, then it works. But that feels like cheating, because you’re putting an equality constraint in, whereas you’re asking to get one out… – Rumpf

@JonPurdy, indeed, in both respects. – Vehemence

Most annoyingly, GHC can't even figure out that either of these implies the other. Trying to go from the fundep version to the type family version gives no way to produce the required type family. Trying to go from the type family version to the fundep version fails the liberal coverage condition (which I take to mean it can't be seen to satisfy the fundeps). – Vehemence

Even if fob were to typecheck, what would stop one from then picking different b and b' and deriving Int :~: Bool? I see one of two possibilities - the context is immediately reduced to C a b, b ~ b' in which case your function becomes trivial, or the function is rejected, because in order to construct that Refl, you must know that b ~ b' but the context is invalid already so any assumptions from it are invalid. I guess the context is a contradiction but ghc doesn't detect that, instead just throwing a type error. – Karttikeya

@user2407038, my understanding is that the functional dependency a -> b forces b ~ b' (but, apparently, neglects to tell anyone so). Yes, the function is then trivial; it was just a (nearly) minimal example. – Vehemence

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.

Karttikeya

I could be wrong, but I think you can already do similarly troubling module tricks using type families and/or GADTs. – Vehemence

I believe those were genuine bugs - you could write those things without assuming the existence of anything. Also, in this case, the compiler still knows about the injectivity, and doesn't allow things to break, even in module D - it is only the assumed function inj_C which is broken. For example x :: (C () Int, C () Bool) => (); x = () does not type check in module D. Perhaps more importantly, neither does x :: forall a b .(C () b, C () a) => (); x = () ! It immediately solves for the type variables and deduces there is a contradiction. – Karttikeya

I don't know that the bug is fixed, and I definitely don't see why the fix wouldn't preclude your example too. What makes this different? – Vehemence

I'm not sure I understand - how would some bug related to type families affect the behaviour of fundeps? Or which bug are you referring to? – Karttikeya

I'm talking about the failure to enforce global coherence when there are diamonds in the module imports. Maybe I'm wrong; I don't have the latest GHC. – Vehemence

Indeed global coherence fails in module D with or without inj_C. However the typechecker still enforces consistency in the sense that the constraints C () Bool and C () Int would both violate the fundep (due to the existence of the other) so these constraints automatically cause a type error. It is only if the compiler can reduce the constraint immediately will it do so. I'm not too sure the exact conditions under which it reduces immediately, but you can prevent the reduction simply by writing the type: also_bad :: C () Bool => Int :~: Bool no longer type checks. – Karttikeya

In short - incoherence is not sufficient to derive false. Incoherence + postulating the existence of inj_C is. I can only conclude that inj_C is the problem, not global incoherence due to funny module imports. – Karttikeya

I see now. Type family incoherence has now, it seems, been banned thoroughly, even for diamond imports, but the same has not been done for fundep violations. Since the fundeps are used only to guide inference, and not for type checking proper, this appears to be safe. Still, it's rather unpleasant, and I'd rather see fundeps follow type families in this regard. – Vehemence

"Still, it's rather unpleasant, and I'd rather see fundeps follow type families in this regard." I agree completely! – Karttikeya

Answer 2

You don't need to resort to multiple modules to fool the functional dependency checker. Here are two examples of wrong fundeps that still build with HEAD. They are adapted from the GHC test suite.

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
             FlexibleInstances, FlexibleContexts,
             UndecidableInstances, DataKinds, PolyKinds,
             GADTs #-}

module M where


data K x a = K x

class Het a b | a -> b where
  het :: m (f c) -> a -> m b
instance Het t t where het = undefined

class GHet (a :: * -> *) (b :: * -> *) | a -> b
instance            GHet (K a) (K [a])
instance Het a b => GHet (K a) (K b)


data HBool = HFalse | HTrue

class TypeEq x y b | x y -> b
instance {-# OVERLAPS #-} (HTrue ~ b)  => TypeEq x x b
instance {-# OVERLAPS #-} (HFalse ~ b) => TypeEq x y b

The fundep checker is still much better than it used to be!

Congius

The first one is badly busted, clearly. The second one seems weird, since b is determined only by the instance context, but is it actually wrong? – Vehemence

Ah. I suppose when the instances are in the same module, as here, it's not really wrong. But you can't convert the two instances to two instances of an open type family encoding the functional dependency. – Congius

Yeah. Well, that's because we have closed type families but not (yet?) closed classes. I suspect overlapping should really always have been done with closed classes (followed immediately by their instances in priority order). A type family associated with a closed class would be closed. – Vehemence

Reid's examples break the FunDep Coverage Condition, so need UndecidableInstances. In the pairs of instances, trying to apply the FunDep Consistency Condition, we can unify the determinants (lhs of FunDep arrow); applying the same substitution into the dependents (rhs) we get bare b; which is not the same as [a]; but is unifiable. We also have a constraint that determines b. GHC can't in general check constraints at instance validation, so it gives up. And I don't want it to be fixed such that that TypeEq test is made invalid. Arguably TypeEq necessarily breaks FunDep Consistency. – Mosa