Opened 2 years ago

Last modified 2 years ago

## #14362 new feature request

# Allow: Coercing (a:~:b) to (b:~:a)

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 8.2.1 |

Keywords: | roles | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Change History (11)

### comment:1 Changed 2 years ago by

### comment:2 Changed 2 years ago by

Reminder

data Coercion a b where Coercion :: Coercible a b => Coercion a b data a :~: b where Refl :: a :~: a

So you want to be able to prove

[W] (a :~: b) ~R# (b :~: a) [W] Coercible a b ~R# Coercible b a

Once could imagine special cases in the compiler, these are really perfectly ordinary data type declarations. What makes these representational type equalities true?

Well, representationally speaking

`Refl :: (a ~# b) => a :~: b`

has no represented value arguments. I suppose that for such types it's true that`(a :~: b) ~R# (c :~: d)`

for any`a, b, c, d`

. Is that right?

Let's think about that first; I expect that once we figure this one out, `Coercible`

will follow.

Richard?

### comment:3 Changed 2 years ago by

Is it not ultimately about implication of constraints (quantified constraints)

-- Witness Constraint data Dict :: Constraint -> Type where Dict :: ctx => Dict ctx instance (ctx => ctx') => Coercible (Dict ctx) (Dict ctx') instance (Coercible a b => Coercible a' b') => Coercible (Coercion a b) (Coercion a' b') instance ((a ~ b) => (a' ~ b')) => Coercible (a:~:b) (a':~:b')

In the case of symmetry,

- To
`coerce :: a:~:b -> b:~:a`

we need to show`a ~ b => b ~ a`

- To
`coerce :: Coercion a b -> Coercion b a`

we need to show`Coercible a b => Coercible b a`

If we think of the class of data types witnessing an `Underlying`

constraint

type family Underlying (dataty :: Type) :: Constraint where Underlying (Dict ctx) = ctx Underlying (Coercion a b) = Coercible a b Underlying (a :~: b) = a ~ b Underlying (a :~~: b) = a ~~ b

we can could write these in a more general form:

instance (Underlying thing => Underlying thing') => Coercible thing thing'

### comment:4 Changed 2 years ago by

A user-defined type with "no represented value arguments" will automatically generate an `Underlying`

type instance

type Cat obj = obj -> obj -> Type data LessThanEq :: Cat Nat where LessThanEq :: a <= b => LessThanEq a b data GreaterThanEq :: Cat Nat where GreaterThanEq :: a >= b => GreaterThanEq a b type instance Underlying (LessThanEq a b) = a <= b type instance Underlying (GreaterThanEq a b) = a >= b

In the magic future, we can coerce

-- ((a <= b) => (a <= 10+b)) => Coercible (LessThanEq a b) (LessThanEq a (10+b)) coerce :: LessThanEq a b -> LessThanEq a (10 + b) -- ((a <= b) => (b >= a)) => Coercible (LessThanEq a b) (GreaterThanEq b a) coerce :: LessThanEq a b -> GreaterThanEq b a

### comment:5 Changed 2 years ago by

Is it not ultimately about implication of constraints?

I don't thuink so. Take `:~:`

. Could I write this function?

convert :: (a :~: b) -> (b :~: a)

Sure! Thus

convert Refl = Refl

Plus, the two represntationns are the same. So yes, they should be coercible. No quantification stuff. I think.

### comment:6 Changed 2 years ago by

But what is the most general type of `convert Refl = Refl`

?

We cannot write

-- Could not deduce: a' ~ b' -- from the context: a ~ b convert :: (a :~: b) -> (a' :~: b') convert Refl = Refl

note how type checking this depends on the ‘underlying constraint’ of `(:~:)`

: `(~)`

.

We must be able to deduce `a' ~ b'`

from the given context `a ~ b`

, which is this?

convert :: ((a~b) => (a'~b')) => (a :~: b) -> (a' :~: b') convert Refl = Refl

so I would expect `coerce`

to have that type.

### comment:7 Changed 2 years ago by

But I don't want the most general type of `convert`

! The general principle of `Coercible`

is that it simply automates what you could do by hand. E.g

newtype Age = MkAge Int convert :: [Int] -> [Age] convert xs = map MkAge xs

And back. So we can reasonably claim `Coercible [Age] [Int]`

.

It's the same with `Coercible (a :~: b) (b :~: a)`

, which is what you asked for. I can do it by hand (with `convert`

); using `coerce`

just automates it.

### comment:8 Changed 2 years ago by

I'm not really sure what this ticket is about. The relation `~R#`

defines representational equality. The rules for this are written in the Coercible paper. There are several other tickets floating about talking about things that are provably `~R#`

, but that GHC's solver can't figure it out. This ticket is different, though: it seems to propose new rules for `~R#`

.

(Note: `Coercible`

is defined as

class a ~R# b => Coercible a b instance a ~R# b => Coercible a b

)

According to the rules for `~R#`

, we don't have `(a :~: b) ~R# (b :~: a)`

: the parameters to `:~:`

both have a nominal role. (Note that role inference looks at constraints as well as other data members, so the `a ~ b`

constraint in the type of `Refl`

is what induces the nominal roles.)

It's conceivable that we could have newtype-GADTs, like

newtype a :~: b where Refl :: a ~ b => a :~: b

With a newtype-GADT, we could imagine forming `(a :~: b) ~R# (b :~: a)`

by unwrapping, using `sym`

and then wrapping using the newtype constructor. (I'm unsure how the solver would work here... but at least it's possible in Core.) Of course, we don't have newtype-GADTs.

And I'm afraid I don't understand what's going on in comment:3 and comment:4. How do these ideas relate to the definition of `~R#`

?

### comment:9 follow-up: 10 Changed 2 years ago by

I'm not really sure what this ticket is about.

It's about the following questions:

- Is
`(a :~: b) ~R# (b :~: a)`

sound? - And if so, what would be its evidence?

Remember we are talking only of when a value of type `(a :~: b)`

can be coerced to one of type `(b :~: a)`

, ust as we speak of coercing a value of type `[Int]`

to one of type `[Age]`

. Curiuosly, the paper doesn't actually articulate the circumstances under which such a coercion is OK -- instead it describes role inference. My sanity check (again not articulated explicitly in the paper) is this: it's sound to coerce a value of type `t1`

into a value of type `t2`

, and vice versa, if

- I could write code of type
`t1 -> t2`

and`t2 -> t1`

- The runtime representations of the two are identical

Both properties hold for `(a :~: b)`

and `(b :~: a)`

, regardless of `a`

and `b`

, don't they? So I claim that `(a :~: b) ~R# (b :~: a)`

is sound.

But `(a :~: a) ~R# (a :~: b)`

obviously must *not* hold, else I could write

good :: forall a. a :~: a good = Refl bad :: forall a b. a -> b bad x = case (coerce (good @ a)) :: a :~: b of Refl -> x

(And, returning to the sanity check, I could not write a function of type `(a :~: a) -> (a :~: b)`

.)

So how *could* we prove `(a :~: b) ~R# (b :~: a)`

?
We have two ways to prove `Coercible`

:

- Decomposition on
`(T ts1) ~R# (T ts2)`

, using the roles of T. That isn't going to work here because it loses the crucial connection bettween`ts1`

and`ts2`

.

- Newtype-unwrapping on
`(N ts1) ~R# t2`

. And (you are way ahead of me as usual), we could do that here if only`:~:`

was a newtype. But, even leaving aside that we don't have newtype GADTs (I think we could maybe fix that), after decomposing both sides we'd have`(a ~ b) ~R# (b ~ a)`

. And now we are back to the original problem: what would be the evidence for such an equality?

### comment:10 Changed 2 years ago by

Replying to simonpj:

- Is
`(a :~: b) ~R# (b :~: a)`

sound?

You have described in your comment a new specification for representational equality: that two types are representationally equal when they are isomorphic and have identical runtime representations. It's too bad we never said that in the paper, because I agree with that specification. The paper then describes an incomplete "implementation" of that specification in its rules for representational equality. This is not the only source of incompleteness. See Appendix A.1 of the extended version of the original ICFP paper.

So, to your question: Is such a thing sound? It would appear to be so, yes. But until we have a full theory that allows such a coercion without breaking something else, I can't be sure.

- And if so, what would be its evidence?

We don't have any representation. And you're right that even if we had newtype-GADTs (which would give a new challenge to the Constraint-vs-Type debate, because they're somewhat the converse of newtype-classes), we couldn't pull this off. (I was wrong on this point, above.) The question is whether `(a ~# b) ~# (b ~# a)`

. Right now, the answer is "no" because we can decompose `(~#)`

. However, Stephanie's new theory *can* handle such things, because it was designed not to be able to decompose `(~#)`

. I'm not intimately familiar with that end of her work, though. (In particular, I know it's forward-compatible with these ideas, but I don't know whether this end of the theory has been worked out in detail.)

My bottom line: GHC's notion of representational equality is useful, but still quite limited. There are lots of ways of expanding it. This is one of them.

### comment:11 Changed 2 years ago by

My bottom line: GHC's notion of representational equality is useful, but still quite limited. There are lots of ways of expanding it. This is one of them.

Agreed. I'm meantally "parking" this.

**Note:**See TracTickets for help on using tickets.

Where the compiler knows constraints (

`(~)`

and`Coercible`

) are symmetric