Should GHC accept a type signature that needs coercion quantification?
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.