[GHC] #9118: Can't eta-reduce representational coercions

[GHC]

#9118: Can't eta-reduce representational coercions
-------------------------------------+------------------------------------
        Reporter:  goldfire          |            Owner:
            Type:  feature request   |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:  #9117
-------------------------------------+------------------------------------
Changes (by nomeata):

 * cc: mail@… (added)
 * related:   => #9117


Comment:

 Wouldn’t you need something like
 {{{
 eta2 :: (forall a. Coercible (f a) (g a)) => Coercion f g
 }}}
 for this to be sound? Oterwise, assuming {{{eta2}}} would typecheck, and
 we had `eta` from #9117 I could write

 {{{
 type family F1 a :: *
 type family F2 a :: *
 type instance F1 Int = Int
 type instance F2 Int = Int
 type instance F1 Bool = Bool
 type instance F2 Bool = Char
 }}}

 and then obtain
 {{{
 let f1eqf2 = eta2 (Proxy :: Proxy Int) :: Coercion F1 F2
     absurd = (eta f1eqf2 :: Coercion (F1 Bool) (F2 Bool)) :: Coercion Bool
 Char
 }}}

 (dry coding, I might be wrong)

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