Turn Coercible into a symmetric relation

[kl0tl]

@rhendric wondered in purescript/purescript-newtype#22 (comment) why Coercible a b doesn’t imply Coercible b a, and indeed it seems like it should.

The Safe Zero-cost Coercions for Haskell paper states in 2 The design and interface of Coercible that Coercible is an equivalence relation and hence should obey the following rules:

► The reflexivity rule: Coercible a a.
► The symmetry rule: If Coercible a b then Coercible b a.
► The transitivity rule: If Coercible a b and Coercible b c then Coercible a c

This is the case in Haskell:

module Example where

import Data.Coerce (Coercible, coerce)
import Data.Proxy (Proxy)

refl :: a -> a
refl = coerce

symm :: Coercible a b => b -> a
symm = coerce

trans :: Coercible a b => Coercible b c => Proxy b -> a -> c
trans _ = coerce

But our Coercible obeys neither symmetry

module Example where

import Safe.Coerce (coerce)
import Prim.Coerce (class Coercible)

symm :: forall a b. Coercible a b => b -> a
symm = coerce

Error found:
in module Example
at Example.purs:7:8 - 7:14 (line 7, column 8 - line 7, column 14)

  No type class instance was found for
                            
    Prim.Coerce.Coercible b0
                          a1
                            

while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
  is at least as general as type b0 -> a1
while checking that expression coerce
  has type b0 -> a1
in value declaration symm

where a1 is a rigid type variable
        bound at (line 7, column 8 - line 7, column 14)
      b0 is a rigid type variable
        bound at (line 7, column 8 - line 7, column 14)

See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
or to contribute content related to this error.

nor transitivity

module Example where

import Safe.Coerce (coerce)
import Type.Proxy (Proxy)
import Prim.Coerce (class Coercible)

trans :: forall a b c. Coercible a b => Coercible b c => Proxy b -> a -> c
trans _ = coerce

Error found:
in module Example
at Example.purs:8:11 - 8:17 (line 8, column 11 - line 8, column 17)

  No type class instance was found for
                            
    Prim.Coerce.Coercible a0
                          c1
                            

while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
  is at least as general as type a0 -> c1
while checking that expression coerce
  has type a0 -> c1
in value declaration trans

where a0 is a rigid type variable
        bound at (line 0, column 0 - line 0, column 0)
      c1 is a rigid type variable
        bound at (line 0, column 0 - line 0, column 0)

See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
or to contribute content related to this error.

[rhendric]

I'm not qualified to catch subtle errors in this part of the code, but from what I can tell it all seems reasonable to me!

Maybe a few more cases worth testing?

• forall b a c. Coercible a b => Coercible c b => Proxy b -> a -> c
• forall a. Coercible a String => a -> NTString1
• forall a. Coercible a (Array String) => a -> Array NTString1

[kl0tl]

I added more tests. Thank you for the suggestion, this made me notice that I wasn’t looking for Coercible dictionaries for the right types 🙈

[hdgarrood]

I'm a little bit unsure about this approach. Could it lead to a loop? Maybe we should be following section 5 of the paper a bit more closely here? Transitivity is hard because it's not always going to be clear what type to pick for b to get from a to c, so I think we should expect the solver to fail to solve Coercible in at least some of the harder cases which require use of transitivity rule. Perhaps we should just do symmetry on its own first?

[rhendric]

Yeah, along those lines, here's a case for which the patch currently produces a PossiblyInfiniteInstance:

test :: forall a b c d. Coercible a c => Coercible a d => Coercible d b => Proxy c -> Proxy d -> a -> b
test _ _ = coerce

The equivalent Haskell works, though I know nothing about how what this patch does differs from what GHC is doing.

If a temporary halfway solution is a good idea, though, wouldn't it be better to have the simpler transitive cases covered with some weirder ones producing PossiblyInfiniteInstance errors then to have all transitive cases produce NoInstanceFound errors?

Maybe a counterargument to that is that this transitive search can produce PossiblyInfiniteInstances where NoInstanceFound would be correct and clearer, in cases like forall a. Coercible a String => a -> Int. Does that matter much? I think maybe it does.

[hdgarrood]

Yeah, I think producing PossiblyInfiniteInstance when we should be producing NoInstanceFound ought to be considered a bug. I think temporary halfway solutions are best avoided in the solver in general, as fixing a temporary halfway solution to work properly might mean that things which used to type check no longer do, and pushing out a change like that is usually going to ruin a few people’s days.

[kl0tl]

Oh that’s no good, I‘ve undone transitivity. Thank you for noticing!

[kl0tl]

For the record, I‘ve read the section 5 Type inference with Coercible constraints of the paper and I‘m trying to rewrite the solver of Coercible constraints to support much richer interactions of givens and wanteds, as explained in the paper.

[rhendric]

@hdgarrood Is there still a chance this will make it into 0.14? I'd like to avoid the churn of a bunch of libraries adding (Coercible t a, Coercible a t) constraints/superclasses (like in the PR linked in the summary) which would just end up being edited down to Coercible t a after a subsequent release.

[hdgarrood]

That's a good point, yes. Let's try to get this into 0.14 then. There's still time - it will take a little while until we are ready to release v0.14.0 properly, as there are still a bunch of library updates which will need doing.

[garyb]

I've encountered a case that will suffer by making this symmetric: Json.

• Every Boolean is Json, but not every Json is Boolean.
• Every String is Json, but not every Json is String.
• etc.

I'm not saying we shouldn't do it still, as perhaps this falls outside the motivation of Coercible as it's a fairly exceptional case, but was this sort of thing considered at all?

[MonoidMusician]

Being able to rewrite arbitrary type parameters safely requires coerce to be a bijection already (proof: the encoding of Leibniz equality). There could be another class for the kind of zero-cost injections you are talking about, which would also include NonEmptyString -> String, but that would be a lot more work, since you would need to keep track of (co/contra)variance and the like if you want the compiler to help out solving those constraints.

Edit: I suppose Leibniz wouldn’t have the right roles to work with coerce, but the point still stands for other types with invariant type parameters, like Store, which might blow up if coerce is not a bijection.

[hdgarrood]

Yes, I would say that Json falls outside the realm of Coercible. It won’t be possible to write any Coercible instances for Json anyway, since the instances are generated on the fly and the compiler forbids you from writing any yourself. In general I think we should aim to follow the safe zero-cost coercions paper as closely as possible, and in the paper Coercible is a symmetric relation, as it only holds where the two types always have the same runtime representation in a way that is verifiable by the compiler.

[garyb]

That all makes sense, 'scuse the silly question!

[hdgarrood]

Not at all, I'm very happy to answer questions :)

[hdgarrood]

Code looks good to me, just a minor quibble about the docs.

[hdgarrood]

I think there should be a comma after "itself" here, as at the moment it sounds like the definition of reflexivity is "any type has the same representation as itself and symmetry", which doesn't really make sense. Although even with that comma, it's still a bit clunky. I think it might be best to address symmetry in a separate paragraph:

First, Coercible obeys reflexivity - any type has the same representation as itself:

  instance coercibleReflexive :: Coercible a a

Second, Coercible obeys symmetry - if a type a can be coerced to some other type b, then b can also be coerced back to a:

instance coercibleSymmetric :: Coercible a b => Coercible b a

[kl0tl]

I wanted to avoid updating the following rules numbering but this is way better.