Haskell Functional Dependencies Consistency Condition: is it needed? Is it used?

The FunDep Consistency Condition appears in all the literature dating back to Mark P Jones 2000 paper. And it's inherited from the database-theory origins of FunDeps.

But Haskell's FunDeps are not very much like in databases: a FunDep -> means: in any instance for this class, I promise to give an algorithm to get from the class parameters on the left to those on the right. (In the instance decl, that algorithm might have to go via its constraints -- then you need UndecidableInstances.)

->

UndecidableInstances

It's reasonably well-known that GHC's implementation of the Consistency Condition is bogus -- see this answer, for example. And that's a Good Thing so that I can write

class TypeEq a a' (b :: Bool) | a a' -> b where ...
instance TypeEq a a True where ...
instance (b ~ False) => TypeEq a a' b where ...


(That needs OverlappingInstances or pragmas, as well as Undecidable.)

OverlappingInstances

Undecidable

The claims in the papers -- including in the FunDeps via CHRs 2006 paper -- is that the Consistency Condition is needed to ensure confluent type inference. And there's an inference rule that if you have TypeEq alpha1 alpha2 beta1 and TypeEq alpha1 alpha2 beta2, you can conclude beta1 == beta2 in which == is type identity not merely ~ unifiability.

TypeEq alpha1 alpha2 beta1

TypeEq alpha1 alpha2 beta2

beta1 == beta2

==

~

But I see no evidence GHC ever applies that rule. And a constraint like this works just fine (EDIT: my first signature here was a bit too in-your-face even for GHC, corrected):

f :: (TypeEq a a' True, TypeEq a' a False) => a -> a' -> ()
f _ _ = ()

f 'c' 'd' -- produces `()` happily


The comparable function using type families can be defined but can't be used

g :: ((a == b) ~ False, (b == a) ~ True) => a -> b -> ()


(Needs TypeOperators, import Data.Type.Equality)
For g 'c' 'd' or g 'c' "d" GHC complains Couldn't match type 'True with 'False.

TypeOperators

import Data.Type.Equality

g 'c' 'd'

g 'c' "d"

Couldn't match type 'True with 'False

Then is the Consistency Condition anything but a nuisance? (There's a few tickets on Trac where it's produced very odd behaviour.)

Does anybody rely on it? Or use it to validate their instances in case of awkward overlaps?

ADDIT: You might think that signature for f is cheating, by flipping the type params. This signature (my initial post)

f

f :: (TypeEq a a' True, TypeEq a a' False) => a -> a' -> ()


Gets rejected Couldn't match type 'False with 'True. So looks like GHC is applying the call-with-same-arguments inference rule.

Couldn't match type 'False with 'True

But this with the args non-flipped goes OK (because the two signatures are too remote?)

f1 :: (TypeEq a a' False) => a -> a' -> [()]
f1 _ _ = [()]
f2 :: (TypeEq a a' True) => a -> a' -> [()]
f2 _ _ = [()]
-- f3 :: (TypeEq a a' f2', TypeEq a a' f1') => a -> a' -> [()]
f3 x y = f1 x y ++ f2 x y


That is, goes OK if I don't put a signature for f3. (And no matter what signature I try for f3, rejects Overlapping instances for TypeEq a b 'True arising from a use of ‘f2’; amongst other messages.)

f3

f3

Overlapping instances for TypeEq a b 'True arising from a use of ‘f2’

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.