[GHC] #14386: GHC doesn't allow Coercion between partly-saturated type constructors

24 Oct 2017

      #14386: GHC doesn't allow Coercion between partly-saturated type constructors
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.3
           Keywords:  roles          |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 If I define an "opposite category" `newtype Op cat a b = Op (cat b a)`
 then representationally it forms an involution: applying `Op` twice gives
 the same representation as not applying it at all

 {{{
 $ ... -ignore-dot-ghci
 GHCi, version 8.3.20170920: http://www.haskell.org/ghc/  :? for help
 Prelude> import Data.Coerce
 Prelude Data.Coerce> import Data.Type.Coercion
 Prelude Data.Coerce Data.Type.Coercion> newtype Op cat a b = Op (cat b a)
 Prelude Data.Coerce Data.Type.Coercion> :t coerce :: Op (Op cat) a b ->
 cat a b
 coerce :: Op (Op cat) a b -> cat a b :: Op (Op cat) a b -> cat a b
 Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op
 cat) a b) (cat a b)
 Coercion :: Coercion (Op (Op cat) a b) (cat a b)
   :: Coercion (Op (Op cat) a b) (cat a b)
 }}}

 But these don't work:

 {{{
 Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op
 cat) a) (cat a)

 <interactive>:1:1: error:
     • Couldn't match representation of type ‘Op (Op cat1) a1’
                                with that of ‘cat1 a1’
         arising from a use of ‘Coercion’
     • In the expression: Coercion :: Coercion (Op (Op cat) a) (cat a)
 Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op
 cat) cat

 <interactive>:1:38: error:
     parse error (possibly incorrect indentation or mismatched brackets)
 Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op
 cat)) cat

 <interactive>:1:1: error:
     • Couldn't match representation of type ‘cat1’
                                with that of ‘Op (Op cat1)’
         arising from a use of ‘Coercion’
       ‘cat1’ is a rigid type variable bound by
         an expression type signature:
           forall (cat1 :: * -> * -> *). Coercion (Op (Op cat1)) cat1
         at <interactive>:1:13-38
     • In the expression: Coercion :: Coercion (Op (Op cat)) cat
 }}}

 I'm wondering if this is intentional

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