Kinds aren't checked in the coverage condition

Following on from the debate in #9103 (closed) (but you don't need to read that ticket), I found a curiosity.

The following module fails to compile, complaining about the unsatisfied coverage condition:

{-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies,
             FlexibleInstances, UndecidableInstances #-}

module Bug where

data Succ a

class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab, a ab -> b
instance (Add a b ab) => Add (Succ a) b (Succ ab)

With -fprint-explicit-kinds, I get

Bug.hs:9:10:
    Illegal instance declaration for
      ‘Add * k * (Succ k a) b (Succ k ab)’
      The liberal coverage condition fails in class ‘Add’
        for functional dependency: ‘a b -> ab’
      Reason: lhs types ‘Succ k a’, ‘b’
        do not jointly determine rhs type ‘Succ k ab’
    In the instance declaration for ‘Add (Succ a) b (Succ ab)’

But, when I add k3 to the right-hand side of the first functional dependency (viz.

{-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies,
             FlexibleInstances, UndecidableInstances #-}

module Bug where

data Succ a

class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab k3, a ab -> b
instance (Add a b ab) => Add (Succ a) b (Succ ab)

) I get

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, modules loaded: Bug.

I always assumed that fixing a type in a fundep also fixed its kind.

I get the same behavior in 7.8 as in 7.10.1RC2.

Trac metadata

Trac field	Value
Version	7.10.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture