Functional dependencies in a particular case

Question

As an introduction, see this question and my answer. I note at the end that it seems that you could remove the need for extraneous type specification with a functional dependency. Here is the code as it stands:

{-# LANGUAGE GADTs, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}

data Nil
data TList a b where
    TEmpty :: TList Nil Nil
    (:.) :: c -> TList d e -> TList c (TList d e)
infixr 4 :.

class TApplies f h t r where
    tApply :: f -> TList h t -> r

instance TApplies a Nil Nil a where
    tApply a _ = a

instance TApplies f h t r => TApplies (a -> f) a (TList h t) r where
    tApply f (e :. l) = tApply (f e) l]

Now, the intuitive thing for me to do seems to be to add the fundep f h t -> r to the TApplies typeclass. However, when I do this, GHC complains about the recursive instance of TApplies as follows:

Illegal instance declaration for
‘TApplies (a -> f) a (TList h t) r’
The coverage condition fails in class ‘TApplies’
   for functional dependency: ‘f h t -> r’
Reason: lhs types ‘a -> f’, ‘a’, ‘TList h t’
   do not jointly determine rhs type ‘r’

The last two lines seem wrong to me, although I expect I simply misunderstand something. My reasoning is as follows:

1. If we have a -> f and a, then we have f.
2. If we have TList h t then we have h and t.
3. Since we have TApplies f h t r, we have the fundep f h t -> r.
4. Therefore, because we have f, h and t, we have r.

This implies to me that the functional dependency is satified. Can someone point out the flaw in my logic, and also perhaps suggest a more apt choice of functional dependency? (Note that something like f r -> h is permitted by GHC but does not seem to provide much leeway in type indication.)

Answer 1

Firstly, I have no idea why you are using such a complicated datatype - so I'll use a simplified one to address your question. The same principle applies to your exact scenario, however.

Define the datatype simple as:

data TList (xs :: [*]) where 
  Nil :: TList '[]
  (:.) :: x -> TList xs -> TList (x ': xs) 

infixr 4 :.

Then your class has one less type parameter:

class TApplies f (xs :: [*]) r | f xs -> r where ...

and the problematic instance would look like

instance TApplies g ys q => TApplies (y -> g) (y ': ys) q where 

Now, examine the error this produces (it is essentially the same as in your question) - namely, note that it says "The coverage condition fails in class `TApplies'". So what is this "Coverage condition"? The user guide has this to say:

The Coverage Condition. For each functional dependency, tvsleft -> tvsright, of the class, every type variable in S(tvsright) must appear in S(tvsleft), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration.

This is overly technical, but basically it says that the set of type variables in the right hand side - in this case, that is {q}, must be a subset of the set of variables in the left hand side - here {y, g, ys}. This is obviously not the case.

You will notice that the coverage condition says nothing about the context of the instance. This is the root of your problem! The context is not considered when deciding if the functional dependency holds. I think you would agree with me that it obviously fails for the instance instance TApplies (y -> g) (y ': ys) q where ..., which is what the compiler sees.

The solution is simple: add {-# LANGUAGE UndecidableInstances #-} to the top of your file. The purpose of the coverage condition, among other things, is to ensure instance resolution is terminating. If you enable UndecidableInstances, you are saying "trust me, it terminates".

---

As a side note, the current formulation is not very nice to use. For example, tApply (+) (1 :. 2 :. Nil) produces an "ambiguous type" error, or something of the sort. Even worse, tApply (+) (1 :. "s" :. Nil) produces the same exact "ambiguous type" error! Not very helpful for anyone trying to write code with this class. You would have to specify monomorphic type signatures everywhere to get it to work as-is.

The solution is to chance the instance declarations to the following:

instance (a ~ a') => TApplies a '[] a' where
instance (TApplies g ys q, y ~ y') => TApplies (y -> g) (y' ': ys) q where 

Then, the first case compiles as is, type defaulting kicks in, and prints "3". In the second case, you get No instance for (Num [Char]), which is actually helpful.

The reason this works is, again, that instance resolution only cares about the instance head, not the context. instance TApplies (y -> g) (y' ': ys) q is what the compiler sees, and obviously y and y' can be any, unrelated, types. It is only at the end, when it is time to print the value, that the compiler needs to resolve the y ~ y' constraint, at which point you simply have the expression (+) 1 2.

---

You can implement your type without data kinds as follows:

{-# LANGUAGE GADTs #-}
data Cons a b 
data Nil

data TList xs where
  Nil  :: TList Nil
  (:.) :: x -> TList xs -> TList (Cons x xs)

There is no real reason to do this, however, since DataKinds cannot break otherwise working code.