Typechecking of dependently-kinded type family instances doesn't have enough equalities in scope

Summary

When typechecking a type family instance, the compiler will ignore some type family instances defined in the current module.

Steps to reproduce

A.hs:

{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
module A where
import Data.Kind

type family Result k :: Type
type family Apply (f :: k) :: Result k

data TyCon = DataCon
type instance Result TyCon = Type

B.hs:

{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
module B where
import A

type instance Apply 'DataCon = Int

This compiles fine. If however we move the contents of B into A like this: A.hs:

{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
module A where
import Data.Kind

type family Result k :: Type
type family Apply (f :: k) :: Result k

data TyCon = DataCon
type instance Result TyCon = Type

type instance Apply 'DataCon = Int

Now suddenly we get an error:

[1 of 2] Compiling A                ( A.hs, A.o )

A.hs:11:32: error:
    • Expected kind ‘Result TyCon’, but ‘Int’ has kind ‘*’
    • In the type ‘Int’
      In the type instance declaration for ‘Apply’
   |
11 | type instance Apply 'DataCon = Int
   |                                ^^^

More curiously, if we enable TemplateHaskell, we can stick a splice inbetween the two instances and it typechecks again:

...
data TyCon = DataCon                                                            
type instance Result TyCon = Type                                               
$mempty                                                                         
type instance Apply 'DataCon = Int   

More interestingly, this works:

data TyCon = DataCon
$mempty
type family Result k :: Type
type family Apply (f :: k) :: Result k
type instance Result TyCon = Type
type instance Apply 'DataCon = Int

Expected behavior

Something. Not this.

Environment

• GHC version used: 8.10.4, 9.0.1