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

mentioned in issue #9103 (closed)

changed weight to 5

added Tbug Trac import labels

As a further curiosity, both versions of the program above fail without UndecidableInstances. How does UndecidableInstances affect the coverage condition check? Is this documented?

mentioned in commit 49d9b009

Sorry for the slightly garbled commit message, but the main payload is right!

Trac metadata

Trac field	Value
Test case	→ typecheck/should_compile/T10109

added 1 deleted label

closed

changed milestone to %7.10.2

This was actually merged a while back; just not closed (see d5c08920).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added FunctionalDependencies label

added Pnormal label