#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 -------------------------------------+------------------------------------ Description changed by simonpj: Old description:

When I say

{{{ import Data.Type.Coercion import Data.Coerce import Data.Proxy

eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g eta2 _ = Coercion }}}

I get

{{{ Could not coerce from ‘f’ to ‘g’ because ‘f’ and ‘g’ are different types. arising from a use of ‘Coercion’ from the context (Coercible (f a) (g a)) bound by the type signature for eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g at /Users/rae/temp/Roles.hs:5:9-56 In the expression: Coercion In an equation for ‘eta2’: eta2 _ = Coercion }}}

Unlike the case for #9116, this one is ''not'' expressible in Core. (At least, I don't see a way to do it.) So, to do this, we would have to update Core and then update the constraint solver. I ''do'' think this would be type safe. But, I also think it's reasonable to wait for someone with a real use case to shout before doing this. The only use case I have is to be able to do this:

{{{ -- says that a's parameter is representational class Rep (a :: k1 -> k2) where co :: Coercible x y => Coercible (a x) (a x)

instance Rep f => Rep (Compose f) where ... }}}

New description: When I say {{{ import Data.Type.Coercion import Data.Coerce import Data.Proxy eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g eta2 _ = Coercion }}} I get {{{ Could not coerce from ‘f’ to ‘g’ because ‘f’ and ‘g’ are different types. arising from a use of ‘Coercion’ from the context (Coercible (f a) (g a)) bound by the type signature for eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g at /Users/rae/temp/Roles.hs:5:9-56 In the expression: Coercion In an equation for ‘eta2’: eta2 _ = Coercion }}} Unlike the case for #9117, this one is ''not'' expressible in Core. (At least, I don't see a way to do it.) So, to do this, we would have to update Core and then update the constraint solver. I ''do'' think this would be type safe. But, I also think it's reasonable to wait for someone with a real use case to shout before doing this. The only use case I have is to be able to do this: {{{ -- says that a's parameter is representational class Rep (a :: k1 -> k2) where co :: Coercible x y => Coercible (a x) (a x) instance Rep f => Rep (Compose f) where ... }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9118#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 -------------------------------------+------------------------------------ Comment (by nomeata): Possibly; I’m don’t know all the details of type families. What `eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g` says is: If `f` and `g` are the same for one arbitrary argument, they must be the same function. Maybe this is the case if type families are excluded for syntactical reasons. In that case, isn’t this an instance of #8555? We are given a more complex constraint `Coercible (f a) (g a)` and want to decompose it to the simpler `Coercible f g`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9118#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 -------------------------------------+------------------------------------ Comment (by goldfire): I agree with rwbarton on this -- I think the `F1`/`F2` example doesn't really apply. But, there remains a problem case: {{{ newtype Pair a = Mk (a, a) }}} We can easily derive `Coercible (Pair Int) ((,) Int Int)`, but it would be bad to derive `Coercible Pair ((,) Int)`. The problem is that the newtype definition has a repeated variable on the right, and thus the definition cannot be eta-reduced. Probably, a sufficiently complicated Core construction can detect and avoid this case, but I don't think it would be easy. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9118#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9118: Can't eta-reduce representational coercions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9117 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => Roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9118#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler