Opened 2 years ago

Last modified 23 months ago

#14386 new bug

GHC doesn't allow Coercion between partly-saturated type constructors

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.3
Keywords: roles Cc:
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:

Description

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

Change History (7)

comment:1 Changed 2 years ago 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.

comment:2 Changed 2 years ago by Iceland_jack

I wondered because we allow

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.

comment:3 Changed 2 years ago 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 a b)

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.

Last edited 2 years ago by nomeata (previous) (diff)

comment:4 in reply to:  3 Changed 2 years ago by Iceland_jack

Replying to 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

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?

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

comment:5 Changed 2 years ago 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.

comment:6 Changed 2 years ago 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.

comment:7 Changed 23 months ago by RyanGlScott

I think ultimately this ties back to GHC's inability to eta-reduce the unwrapping rule:

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.

Note: See TracTickets for help on using tickets.