Should GHC accept a type signature that needs coercion quantification?

Consider

f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x
f = error "uk"

Should we accept it? Now that we have coercion quantification (Trac #15497 (closed)), I think the answer should be yes, with the elaborated signature being

f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x

But there is a problem: the user wrote k ~ (k1 -> *), and that's a boxed value that we can't take apart in types. I'm not sure what to do here.

See also:

• These thoughts arose when contemplating Note [Emitting the residual implication in simplifyInfer] in TcSimplify; see ticket:15710#comment:161240 in #15497 (closed)

• This page about homogeneous equality, esp "A small wrinkle".

• #27168 (closed)