Implement `Coercible` for safe zero-cost coercions

[lunaris]

This PR adds Coercible for safe zero-cost coercions, as per the similar feature in GHC Haskell. It's intended to be the first step towards implementing deriving via (#3302). Compiler support only boils down to the constraint Coercible -- the actual function coerce :: forall a b. Coercible a b => a -> b can be implemented in library code (as unsafeCoerce, thus receiving the same inlining/elimination treatment and so being zero-cost). The tests will fail because of this point because I need to find a place to put Safe.Coerce (the module which exposes coerce). Happy to take input on how to best accomplish this.

Changes

• Define a new built-in module, Prim.Coerce which exports a single
  type class, Coercible a b, which relates types with identical runtime
  representations.

• Extend the type checker's class solver to solve constraints of the
  form Coercible a b automatically, as per the rules in the paper "Safe
  Zero-Cost Coercions for Haskell" (though simpler due to the absence of
  some of Haskell's features like type families).

• As part of the above point, add support for role inference to the type
  checker.

[kcsongor]

It looks like this case should mark all t2s as representational:

data F a b = F (a b)

As a is polymorphic, we don't know what its role annotation is going to be, therefore we should be careful and assume that its argument is representational (because it very well could be!).

That means that for F, b would be inferred representational as well.
I think the current implementation will infer phantom for b, allowing to coerce
F Maybe Int and F Maybe String

[kcsongor]

It looks like this case should mark all t2s as representational:

Or rather, just walk all t2s, as that will mark all type variables representational anyway, and ensure that we don't accidentally mark phantom things representational (which would be safe, but undesirable).

So:

data G a b = G (a (Phantom b))

data Phantom a = Phantom

will not get tricked into marking b as representational.

---

Note: this case is actually interesting, because it differs from what GHC does. Not having to consider nominal roles results in a non-trivial difference:

For G above, GHC would infer

type role G representational nominal

This is because with nominal as a possibility, we must assume that a's argument can be nominal, therefore Phantom b is in a nominal role. However, nominal is "infectious": if Phantom b is nominal, then all type variable therein must be nominal too (b here). This being the case, GHC rightly marks b as nominal, and stops. In the paper, this is accounted for by the rules that mark all free variables nominal.

However, with only phantom and representational roles, we can do better than simply downgrading nominal to representational! Phantom b being in a representational role doesn't "infect" b: walking is sufficient to determine the above result.

As a result, GHC would never allow to coerce between G Maybe Int and G Maybe String - but we can!

[kcsongor]

What happens with mutually recursive types?

data F a = F (G a)
data G a = G (F a)

[kcsongor]

This use of lookup seems like we're taking the role of the first occurrence of a in the constructors.

Does it mean that for

data Phantom a = Phantom

data F a = MkF (Phantom a) a

we get

type role F phantom

?

[lunaris]

I thought you were right but after some testing I think I actually get away with this due to the fact that Phantom parameters are not realised at all. E.g. for the types:

data Phantom a = Phantom
data F a = MkF (Phantom a) a

walking the MkF constructor for F yields:

[ [], [("a", Representational)] ]

That is, the Phantom use results in [], not ("a", Phantom). So this works. I think this is OK but am open to alternative implementations.

[kcsongor]

Ah, you're right - I missed this. Perhaps then walk should just return a list of representational types? (as it already does, but its type is somewhat misleading)

[rightfold]

Without explicit role annotations, how can the programmer ensure safety when using phantom types that should prevent coercibility? There are many thinkable instances of this with the FFI.

[kcsongor]

@rightfold you certainly raise a good point, I would imagine that by default all arguments to foreign types have to be representational

[lunaris]

I've implemented @kcsongor's suggestion to infer Representational for all foreign declarations though will look into how cheaply I can implement role signatures (let the bikeshedding begin).

[paf31]

I like the idea of using Representational as the default. Generally, I like the idea of keeping roles hidden from the user entirely.

[lunaris]

As it currently stands that's what this branch does now. I've prototype role declarations in another branch but that's a separate discussion I think.

[lunaris]

I've rebased this on master; can we make any progress on merging it? As noted, we'd need to decide:

• Module and package to expose coerce -- currently I've hacked a Safe.Coerce module into purescript-unsafe-coerce in the tests/support/bower_components directory to make the tests/purs/passing/Coercible.purs test pass. Implementation is just:

module Safe.Coerce (coerce) where

import Prim.Coerce (class Coercible)
import Unsafe.Coerce (unsafeCoerce)

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

• If we are happy with the situation regarding roles and their inference etc., which it sounds like we might be. Not sure though.

[vladciobanu]

Just a minor note, I think most of Environment.hs was recently (0.12) updated to have more descriptive names for type parameters. I think it might help newcomers if a and b were from and to, or something similar.

Other than that, this looks good to me and I hope it gets merged soon.

[LiamGoodacre]

I'll do a proper review tonight.

[LiamGoodacre]

I'll do a proper review tonight.

[LiamGoodacre]

The example code here and later on aren't in PureScript syntax (no instance naming). What do you think about:

instance reflexivity :: Coercible a a

[LiamGoodacre]

In data T a = T (forall a. a -> a) will this produce Representational a, when it should be Phantom?

[LiamGoodacre]

Shouldn't these be a' and b'?

[LiamGoodacre]

Just tried this situation and got no instance found via gToGN:

-- existing tests
data G a b = G (a (Phantom2 b))
gToG :: G Maybe Int -> G Maybe String
gToG = coerce

-- new stuff
newtype OptionIn a = OptionIn (Maybe a)
newtype OptionOut a = OptionOut (Maybe a)
gToGN :: G OptionIn Int -> G OptionOut String
gToGN = coerce

[LiamGoodacre]

Following from @kcsongor's earlier comment:

data MutI f a = MutI a (Maybe (f a))
newtype MutA a = MutA (MutI MutB a)
newtype MutB t = MutB (MutI MutA t)

mutAToMutB :: MutA Int -> MutB Int
mutAToMutB = coerce

Gives the error:

          Type class instance for
            Prim.Coerce.Coercible (MutI MutA t1) (MutI MutB t0)
          is possibly infinite.

        while solving type class constraint
          Prim.Coerce.Coercible (MutI MutB t0) MutB

[LiamGoodacre]

The following causes the compiler to loop and eat all your memory 😸

newtype X a = X (X (X a))
xToY :: X Int -> X (X Int)
xToY = coerce

[LiamGoodacre]

Not sure if that previous one is a bug with this or not. As the following also loops:

newtype X a = X (X (X a))
xToY :: X Int -> X (X Int)
xToY = ?ohNo

Will make a new issue for this.