Another case of type families not being reduced

Similar to #12381 (closed) and #11348 (closed) but this one doesn't pass with GHC HEAD either,

{-# LANGUAGE TypeInType, TypeFamilies, FlexibleInstances #-}

import GHC.Types

type family F (a :: Type) :: Type

class C a where
  type D (a :: Type) :: F a

instance (F a ~ Bool) => C a where
  type D a = True

fails with,

Hi.hs:11:14: error:
    • Expected kind ‘F a’, but ‘'True’ has kind ‘Bool’
    • In the type ‘True’
      In the type instance declaration for ‘D’
      In the instance declaration for ‘C a’

Trac metadata

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

changed milestone to %8.0.2

changed weight to 5

added Tbug Trac import typechecker labels

closed

Kosmikus beat me to reporting this. This is a duplicate of #12384 (closed).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

added Pnormal label