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

[GHC]

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

Comment (by RyanGlScott):

 You're asking about two different (incomplete) programs, so I'm forced to
 guess at what your intention was. I'll tackle them in reverse order.

 For the second program, I'm guessing this is what you meant? I had to add
 some imports and language extensions to make this go through:

 {{{#!hs
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}

 import Data.Coerce
 import Data.Functor.Compose
 import Data.Functor.Identity
 import Data.Kind

 (<%<) :: (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

 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 importantly, this program does typecheck! So I'm not sure what bug
 you're alluding to here. (You mention "we can not unify the types of
 `id1F` and `id2F`", but I'm not sure what is meant by that statement.)

 For the first program, I also needed to add some imports and language
 extensions:

 {{{#!hs
 {-# LANGUAGE TypeOperators #-}

 import Data.Functor.Compose
 import Data.Functor.Identity
 import Data.Type.Coercion

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

 fails :: Identity `Coercion` Compose Identity Identity
 fails = Coercion
 }}}

 But this time, I can reproduce the error you reported for this program.
 The error is right on the mark—you can't `coerce` between `Identity` and
 `Compose Identity Identity` because they're not representationally equal.
 Full stop. Try as you might, there's no way to derive a `Coercible
 Identity (Compose Identity Identity)` constraint.

 I think you might be inclined to believe that because `Identity a` is
 representationally equal to `(Compose Identity Identity) a`, that GHC can
 conclude that `Identity` is representationally equal to `Compose Identity
 Identity`. But to my knowledge, there's no reasoning principle which
 states that `f a ~R g a` implies `f ~R g`.

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