## 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.

These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]`

in `TcSimplify`

; see ticket:15710#comment:161240 in #15497 (closed)