Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types

{-# LANGUAGE TypeFamilies, PolyKinds #-}

module A where

data family D :: k

type family F (a :: k) :: *

type instance F (D Int) = Int
type instance F (f a b) = Char
type instance F (D Int Bool) = Char

The last equation, even though a specialization of the middle one, trips up the equality consistency check:

a.hs:9:15: error:
    Conflicting family instance declarations:
      F (D Int) = Int -- Defined at a.hs:9:15
      F (D Int Bool) = Char -- Defined at a.hs:10:15
  |
9 | type instance F (D Int) = Int
  |               ^

So GHC is able to infer that D Int ~/~ f a b because D ~/~ f a, but for some reason the same reasoning doesn't work for D ~/~ D a.

Trac metadata

Trac field	Value
Version	8.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture