Type family equations with wrong name are accepted when the type family has a SAKS

Summary

Type family equations with wrong names are accepted when the type family has a standalone kind signature.

Steps to reproduce

{-# LANGUAGE TypeFamilies, StandaloneKindSignatures #-}

module Bug where

data Bar

type Foo :: *
type family Foo where
  Bar = ()

Bar used in equation is obviously wrong, still ghc compiles the program without an error. -ddump-types reports correct axiom:

COERCION AXIOMS
  axiom Bug.D:R:Foo :: Foo = ()

Expected behavior

I'd expect ghc to reject the program with the same error message it gives if Foo had no SAKS

Bug.hs:7:3: error:
    • Mismatched type name in type family instance.
        Expected: Foo
          Actual: Maybe
    • In the type family declaration for ‘Foo’
  |
7 |   Maybe = ()

Environment

• GHC version used: 9.0.1, 9.3.20210819

Optional:

• Operating System: Linux (NixOS)
• System Architecture: x86-64