[GHC] #14386: GHC doesn't allow Coercion between partly-saturated type constructors
#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
#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 Resolution: | Keywords: roles 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 nomeata): Maybe not quite intentional, but certainly expected. I think the coercion you want is not even expressible at the level of Core, because the newtype gives you the axiom {{{ forall cat a b. Op cat a b ~R cat b a }}} And as you can see you can only use this axiom once `Op` has all three arguments. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14386#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Resolution: | Keywords: roles 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 Iceland_jack): I wondered because we allow {{{#!hs import Data.Type.Coercion newtype USD = USD Int wit :: Coercion (Either USD) (Either Int) wit = Coercion }}} I don't understand Core enough to get the difference, but (prima facie) it doesn't seem wrong to allow `Coercion (Op (Op cat)) cat`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14386#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Resolution: | Keywords: roles 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 nomeata): No, it would not be wrong. We just don't have the machinery yet. Interestingly, had you had {{{ newtype NotOp cat a b = NotOp (cat b a) }}} then `:t Coercion :: Coercion (NotOp (NotOp cat)) cat` would work. Why? Because the axiom you get out of a `newtype` is eta-contracted as far as possible; in this case. {{{ NotOp cat ~ cat }}} The thing with `Either` is a completely different story. Note that you are coercing _an argument of `Either`_ (still `Either` on both sides) whereas originally you are coercing between `Op` and it’s representation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14386#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Resolution: | Keywords: roles 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 Iceland_jack): Replying to [comment:3 nomeata]:
Interestingly, had you had
{{{ newtype NotOp cat a b = NotOp (cat b a) }}} then `:t Coercion :: Coercion (NotOp (NotOp cat)) cat` would work.
Did you mean {{{#!hs newtype NotOp cat a b = NotOp (cat a b) }}}
The thing with `Either` is a completely different story. Note that you are coercing _an argument of `Either`_ (still `Either` on both sides) whereas originally you are coercing between `Op` and it’s representation.
With quantified constraints, could we write? {{{#!hs type OpOp cat = forall xx yy. cat xx yy `Coercible` Op (Op cat) xx yy wit :: OpOp cat => Op (Op cat) `Coercion` cat wit = Coercion }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14386#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Resolution: | Keywords: roles 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 nomeata):
With quantified constraints, could we write?
I don’t think so. It would require a rule “eta-expansion rule” {{{ ∀a. T1 a ~R T2 b −−−−−−−−−−−−−− T1 ~R T2 }}} which does not exist. But others will have to tell you if that can exist or if it would break things. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14386#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Resolution: | Keywords: roles 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 goldfire): This seems to be yet another way representational equality could, theoretically, expand. Note that, unlike certain other problems, this isn't a limitation of the solver, but of the definition of the equality relation itself. It might be helpful to maintain a list of such deficiencies. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14386#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Resolution: | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14317 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14317 Comment: I think ultimately this ties back to GHC's inability to eta-reduce the unwrapping rule: {{{#!hs Coercible (Op cat a b) (cat b a) }}} In other words, it's the same symptom as in https://ghc.haskell.org/trac/ghc/ticket/14317#comment:6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14386#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC