Visible foralls are no longer injective

The following program compiles on GHC HEAD:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

inject :: forall (f :: forall (k :: Type) -> Type)
                 (a :: Type) (b :: Type).
          f a :~: f b
       -> a :~: b
inject Refl = Refl

But on this branch, it fails with this error:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:10:11: error:
    • Couldn't match type ‘f a’ with ‘f0 a’
      Expected type: (f a :~: f b) ~> a :~: b
        Actual type: (f0 a :~: f0 b) ~> a :~: b
    • In the ambiguity check for ‘inject’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        inject :: forall (f :: forall (k :: Type) -> Type)
                         (a :: Type)
                         (b :: Type).
                  f a :~: f b ~> a :~: b
   |
10 | inject :: forall (f :: forall (k :: Type) -> Type)
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Weird, it's complaining that f is ambiguous now. If I enable AllowAmbiguousTypes, then it still fails:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:15:15: error:
    • Could not deduce: a ~ b
      from the context: f b ~ f a
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in an equation for ‘inject’
        at Bug.hs:15:8-11
      ‘a’ is a rigid type variable bound by
        the type signature for:
          inject :: forall (f :: forall k -> *) a b. (f a :~: f b) ~> a :~: b
        at Bug.hs:(11,1)-(14,17)
      ‘b’ is a rigid type variable bound by
        the type signature for:
          inject :: forall (f :: forall k -> *) a b. (f a :~: f b) ~> a :~: b
        at Bug.hs:(11,1)-(14,17)
      Expected type: a :~: b
        Actual type: a :~: a
    • In the expression: Refl
      In an equation for ‘inject’: inject Refl = Refl
    • Relevant bindings include
        inject :: (f a :~: f b) ~> a :~: b (bound at Bug.hs:15:1)
   |
15 | inject Refl = Refl
   |               ^^^^

Something seems deeply strange here.