Pattern matching in type families seemingly treats constructor constraints as wanted instead of as given

Summary

When pattern matching on a constructor that contains a constraint with a type family application (e.g. Not a ~ True => Foo a) in a type family equation, GHC seemingly treats this constraint as wanted rather than as given, leading to a somewhat confusing error message.

Steps to reproduce

Load the following file into GHCi:

{-# LANGUAGE GADTs, TypeFamilies, DataKinds #-}

type family Not b where
  Not True = False
  Not False = True

data Foo a where MkFoo :: Not a ~ True => Foo a
data Bar a where MkBar :: Not a ~ True => Bar a

foo2bar :: Foo a -> Bar a
foo2bar MkFoo = MkBar

type Foo2Bar :: Foo a -> Bar a
type family Foo2Bar foo where
  Foo2Bar MkFoo = MkBar

It produces the error

TyFamGADT.hs:15:11: error:
    * Couldn't match expected kind 'True with actual kind `Not a'
    * In the first argument of `Foo2Bar', namely `MkFoo'
      In the type family declaration for `Foo2Bar'
   |
15 |   Foo2Bar MkFoo = MkBar
   |           ^^^^^

Note that interestingly, if I injectivity annotation is added (type family Not b = r | r -> b where), the error message changes to the completely different

TyFamGADT.hs:15:3: error:
    * Illegal type synonym family application `Not 'False' in instance:
        Foo2Bar
          @'False
          ('MkFoo @'False @{'GHC.Types.Eq# @Bool @(Not 'False) @'True <>})
    * In the equations for closed type family `Foo2Bar'
      In the type family declaration for `Foo2Bar'
   |
15 |   Foo2Bar MkFoo = MkBar
   |   ^^^^^^^^^^^^^^^^^^^^^

Expected behavior

Ideally, this should just work, just like the term-level function. Failing that, the error message could be improved, such that it doesn't look like the constraint is treated as a wanted constraint when you would expect it to be given.

Environment

• GHC version used: 9.6.2, 9.2.5

Optional:

• Operating System: Ubuntu on WSL on Windows 11
• System Architecture: x86_64