Weird behaviour when passing polytypes to type families

Summary

In the type of a definition, passing polytypes to type families seems to lead to all sorts of weird behaviour.

Steps to reproduce

import Data.Proxy (Proxy)
import Data.Kind (Type)

type family F (b :: Bool) (t1 :: Type) (t2 :: Type) :: Type where
  F 'True t1 t2 = t1
  F 'False t1 t2 = t2

-- almost works, but gives error when using:
-- f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: ()). ()) ()
-- f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F 'True (forall (x :: a). ()) ()
-- gives nonsense error when checking ambiguity:
f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()
f = undefined

The error:

Test.hs:11:6: error:
    • Couldn't match type: F b (forall (x :: a). ()) ()
                     with: F b (forall (x :: a). ()) ()
      Expected: Proxy @{Type} a
                -> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
        Actual: Proxy @{Type} a
                -> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
      NB: ‘F’ is a non-injective type family
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        f :: forall (a :: Type) (b :: Bool). Proxy a
                                             -> Proxy b -> F b (forall (x :: a). ()) ()
   |
11 | f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()

With -XAllowAmbiguousTypes:

Test.hs:11:6: error:
    • Couldn't match type: F b (forall (x :: a). ()) ()
                     with: F b (forall (x :: a). ()) ()
      Expected: Proxy @{Type} a
                -> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
        Actual: Proxy @{Type} a
                -> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
      NB: ‘F’ is a non-injective type family
    • In the ambiguity check for ‘f’
      In the type signature:
        f :: forall (a :: Type) (b :: Bool). Proxy a
                                             -> Proxy b -> F b (forall (x :: a). ()) ()
   |
11 | f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()

In the case where it looks like it should work, notably

f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F 'True (forall (x :: a). ()) ()

We get the following behaviour:

>>> :t f 
f :: forall a (b :: Bool).
     Proxy @{Type} a
     -> Proxy @{Bool} b -> F 'True (forall (x :: a). ()) ()

>>> :t f (Proxy @Int)
f (Proxy @Int)
  :: forall {b :: Bool}. Proxy @{Bool} b -> forall (x :: Int). ()

>>> :t f (Proxy @Int) (Proxy @'True)
f (Proxy @Int) (Proxy @'True) :: forall (x :: Int). ()

>>> f (Proxy @Int) (Proxy @'True)
<interactive>:45:1: error:
    • Couldn't match type ‘forall (x1 :: Int). ()’ with ‘()’
      Expected: ()
        Actual: F 'True (forall (x :: Int). ()) ()
    • When checking that the inferred type
        it :: F 'True (forall (x :: Int). ()) ()
      is as general as its inferred signature
        it :: forall (x :: Int). ()

Expected behavior

Either they should work, or give a useful error message. Optimally they would work, since I'm trying to work around returning polytypes from type families.

Environment

• GHC version used: 9.2.3