Solve Coercible constraints over type constructors

The core question is, could fails type check?

import Data.Type.Coercion

works :: Identity a `Coercion` Compose Identity Identity a
works = Coercion

-- • Couldn't match representation of type ‘Identity’
--                            with that of ‘Compose Identity Identity’
--     arising from a use of ‘Coercion’
-- • In the expression:
--       Coercion :: Identity `Coercion` Compose Identity Identity
fails :: Identity `Coercion` Compose Identity Identity
fails = Coercion

---

This arises from playing with Traversable: A Remix.

Given coerce :: Compose Identity Identity ~> Identity I wanted to capture that id1 and id2 are actually the same arrow (up to representation)

(<%<) :: (Functor f, Functor g) => (b -> g c) -> (a -> f b) -> (a -> Compose f g c)
g <%< f = Compose . fmap g . f

id1 :: a -> Identity a
id1 = Identity

id2 :: a -> Compose Identity Identity a
id2 = Identity <%< Identity

So I define

data F :: (k -> Type) -> (Type -> k -> Type) where
  MkF :: Coercible f f' => (a -> f' b) -> F f a b

id1F :: Coercible Identity f => F f a a
id1F = MkF id1

id2F :: Coercible (Compose Identity Identity) f => F f b b
id2F = MkF id2

but we can not unify the types of id1F and id2F. Does this require quantified class constraints? I'm not sure where they would go

Trac metadata

Trac field	Value
Version	8.2.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture