Functional Dependencies

This is the root page for material about functional dependencies in GHC.


Use Keyword = FunDeps to ensure that a ticket ends up on these lists.

Open Tickets:

Weird fundep behavior (with -fallow-undecidable-instances)
"overlapping instances" through FunctionalDependencies
GHC does not check the functional dependency consistency condition correctly
Allow class associated types to reference functional dependencies
Allow wildcards for parameters functionally determined (also type synonyms)
Ambiguous types in pattern synonym not determined by functional dependencies
Can't capture improvement of functional dependencies
Check if constraint synonym satisfies functional dependencies
GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loop
Functional dependency conflicts in givens
FunDep origin not correctly attributed
Undependable Dependencies
Weird interaction between fundeps and overlappable instances

Closed Tickets:

Do a better job of solving recursive type-class constraints with functional dependencies
Panic "lookupVarEnv_NF" when using a functional dependency with a kind variable
erroneous overlapping instances reported with FunDeps
Panic "ctEvTerm" when using functional dependencies and PolyKinds
ghc panic: varargs + sets
Kinds aren't checked in the coverage condition
GHC 7.10.2 RC cannot build HList-
Terrible error message with fundeps and PolyKinds
Kind-level functional dependencies are not resolved properly
Incorrect behavior with empty functional dependencies
Spurious extra error message due to functional dependencies
Singletons code fails to typecheck when type signature involving type family is added
Type error in program caused by unrelated definition
GHC 8.4.1-alpha regression with FunctionalDependencies
Functional dependencies can get GHC to print "UnkSkol"

Consistency of Functional Dependencies

(This section was written by Iavor; I am unsure of its current status. SLPJ Apr 17.)

The functional dependencies on a class restrict the instances that may be declared for a given class. The instances of a class:

    class C a b c | b -> c where f :: ...

are consistent with its functional dependency if the following invariant holds:

    byFD(C,1): forall a1 a2 b c1 c2. (C a1 b c1, C a2 b c2) => (c1 ~ c2)

Please note that the question of FD-consistency is orthogonal to instance coherence (i.e, uniqueness of evidence, overlapping instances, etc.), and the decidability of type-checking of terms---for examples of their independence, please see the Examples at the end of the document.

If we check that all instances in scope are consistent with their FDs, then we can use the FD invariant byFD during type inference to infer more precise types, report errors involving unsolvable contexts, or accept programs that would be rejected without the invariant.

For example, if we have an instance:

  I: instance F Int Int Char

and we have a constraint C: F Int Int a, then we can use the FD-invariant to prove that a must be Char:

    byFD(C,1) (C,I) :: a ~ Char

Checking FD-Consistency

To ensure FD-consistency, before accepting an instance we need to check that it is compatible with all other instances that are already in scope. Note that we also need to perform the same check when combining imported instances. Consider adding a new instance to an FD-consistent set of instances:

    I: instance P(as,bs) => C t1(as,bs) t2(as) t3(as,bs)

The notation t(as) states the variables in t are a subset of as.

  1. Check that I is self-consistent (i.e., we can't use different instantiations of I to violate FD-consistency). Self consistency follows if we can prove the following theorem:
             forall as bs cs. (P, P[cs/bs]) => t3[cs/bs] ~ t3[cs/bs]
  2. Check that I is FD-consistent with all existing instances of the class. So, for each existing instance, J:
             J: instance Q(xs) => C s1(xs) s2(xs) s3(xs)
    we need to show that:
             forall as bs xs. (P,Q,s2 ~ t2) => (s3 ~ t3)
    Assuming no type-functions in instance heads, the equality assumption is equivalent to stating that s2 and t2 may be unified, so another way to state our goal is:
             forall as bs xs. (P[su], Q[su]) => (s3[su] ~ t3[su])
    where su is the most general unifier of s2 and t2.

Proving these two goals before accepting an instance is similar to the process of finding evidence for super-classes before accepting and instance. Also, note that while proving (2), it is not a problem if we find that we have assumed a contradiction: this simply means that the two instances can never be used at the same time, so the FD-consistency follows trivially.


  • FD-consistency is orthogonal to instance coherence.

FD-consistent but not coherent:

         instance C Int Int Int where f = definition_1
         instance C Int Int Int where f = definition_2

Coherent but not FD-consistent:

         instance C Int  Int Char where ...
         instance C Char Int Bool where ...
  • FD-consistency is orthogonal to termination of instances.

FD-consistent but "non-terminating":

         instance C a b c => C a b c

Terminating but not FD-consistent:

         instance C Int  Int Char where ...
         instance C Char Int Bool where ...
Last modified 2 years ago Last modified on Apr 13, 2017 11:53:49 AM