Dependent type families cannot be separated from their instances

Summary

I'm doing experiments with some very dependently typed type families. It works all nice when everything is in a single file, but not when trying to split it into different modules.

Steps to reproduce

Minimal example: two type families F and G, where G's second argument depends on the first, and one instance for each family.

{-# LANGUAGE TypeFamilies #-}
module A where
import Data.Kind (Type)

type family F (x :: Type) :: Type
type family G (x :: Type) (y :: F x) :: Type

type instance F () = Type
type instance G () k = k

That compiles (tried on GHC 9.4). But if we move the last two lines to another module, we get:

B.hs:9:20: error:
    • Expected kind ‘F ()’, but ‘k’ has kind ‘*’
    • In the second argument of ‘G’, namely ‘k’
      In the type instance declaration for ‘G’
  |
9 | type instance G () k = k
  |

If we then move the last line to yet another module, it compiles again.

It seems that when typechecking the G instance, GHC somehow does not see F's instance.

Even more weirdness: this behavior is not stable under expansion/folding of type synonyms.

The following refactoring of the instances does compile when separated from the family declarations:

type W = ()

type instance F () = Type
type instance G W k = k

(And other combinations of W and () don't compile.)

Expected behavior

These declarations should compile regardless of whether they are in separate files.

Environment

• GHC version used: 9.0, 9.2, 9.4