[GHC] #14317: Solve Coercible constraints over type constructors

[GHC]

#14317: Solve Coercible constraints over type constructors
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The core question is, could `fails` type check?

 {{{#!hs
 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
 [https://duplode.github.io/posts/traversable-a-remix.html 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)

 {{{#!hs
 (<%<) :: (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

 {{{#!hs
 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

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14317>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler