Using KProxy as argument fails ambiguity check

[jstolarek]

data KProxy (a :: *) = KProxy
type family G (kproxy :: KProxy k) = r | r -> k

foo :: G 'KProxy -> G 'KProxy
foo x = x

This definition fails the ambiguity check but I believe it shouldn't.

Couldn't match expected type ‘G k1 ('KProxy k1)’
            with actual type ‘G k ('KProxy k)’
NB: ‘G’ is a type function, and may not be injective
Relevant bindings include
  x :: G k ('KProxy k) (bound at T6018.hs:40:5)
  foo :: G k ('KProxy k) -> G k1 ('KProxy k1)
    (bound at T6018.hs:40:1)
In the expression: x
In an equation for ‘foo’: foo x = x

[jstolarek]

Closing as invalid. Richard explains:

The problem is how GHC interprets the type G 'KProxy -> G 'KProxy. After kind-checking & desugaring, this becomes, with explicit kind arguments: G k1 ('KProxy k1) -> G k2 ('KProxy k2). This type clearly does not classify the identity function. The problem is that the solver is run "too late" here. By the time the injectivity annotations are processed, the type has already been desugared, with an extra degree of freedom. (...) try this:

foo :: G ('KProxy :: KProxy k) -> G ('KProxy :: KProxy k)

That should eliminate the unwanted degree of freedom.