#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