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

### comment:2 Changed 2 years ago by

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 follow-up: 4 Changed 2 years ago by

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.

### comment:4 Changed 2 years ago by

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

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

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

Related Tickets: | → #14317 |
---|

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.

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

And as you can see you can only use this axiom once

`Op`

has all three arguments.