Does a one way version of Coercible exist? For example if I have
newtype Prime = MkUnsafePrime Int
mkPrime :: Int -> Maybe Prime
Then I want something like instance CoercibleOneWay Prime Int with coerceOneWay :: CoercibleOneWay a b -> a -> b. With Coercible I either get both directions (if the constructor is in scope) or neither direction (if it’s not). Surely we can do better. Has anyone done something like that yet?
I think that’s what witch is all about. For converting primes to ints you could make an instance From Int Prime, and it also has a TryFrom class that you could create a TryFrom Prime Int instance for.
witch is about conversions indeed, but I’m looking for zero cost conversions specifically.
Witch defaults to using coerce unless you provide an implementation for from. In other words I think instance From Prime Int should be zero cost.
Sure, but the problem in this case is that I can’t bring the Coercible instance into scope (i.e. I can’t export the constructor) because that’s unsafe. It’s not valid to coerce from an Int to a Prime!
My question is whether there exists a more refined notion of Coercible that only works in one direction.
You can’t export a function fromPrime = coerce :: Prime -> Int?
That’s not zero cost. For example, with coerce I can do
coerce :: [Identity Int] -> [Int]
I could also do
coerce :: [Prime] -> [Int]
but that comes at the cost of also allowing
coerce :: [Int] -> [Prime]
which is invalid. Ideally I’m looking for something that supports
coerceOneWay :: [Prime] -> [Int]
without also supporting [Int] -> [Prime].
That’s not zero cost.
Presumably that function would be inlined?
When I want to constrain coerce, I usually resort to an auxiliary type family to guide the conversion. But I’m unsure about how to do it for newtypes in general 
Exporting a function to do the conversion is not enough to be zero cost, regardless of whether its inlined, because you don’t want to just be able convert a single Prime to an Int, but containers of Primes to a containers of Ints, functions returning containers of Primes to functions returning containers of Ints etc. . That’s the point of Coercible.
fmap from :: [Prime] -> [Int] appears to be zero cost for me with -O1 even when MkUnsafePrime isn’t exported.
Sure, but in general this kind of thing is not zero cost. That’s the whole point for Coercible to exist in the first place.
For more info see the introduction to the original paper: https://www.seas.upenn.edu/~sweirich/papers/coercible.pdf
There was a little discussion of this before: Unidirectional Coercible · Issue #198 · ghc-proposals/ghc-proposals · GitHub
I think it’s a perfectly sensible feature request, but doing it “properly” would require a nontrivial amount of surgery to Core’s coercion system and GHC’s constraint solver (basically removing the symmetry constructor and making sure that all proof rules have symmetric forms where appropriate). One could of course experiment with doing it in a type-checker plugin.
I’ve also come across this package, which provides functions for doing this explicitly rather than using a class to infer the coercions: coercible-subtypes: Coercible but only in one direction
Thanks Adam, that’s very helpful. I can get a long way at the library level by wrapping Coercible but ultimately I’ll need to deduce (Sub a' a, Sub b b') => Sub (D a b) (D a' b') for things like data D a b = D (a -> b), so I suspect I will eventually need compiler support (maybe TH would be good enough).
One-way coercibles would also be useful for modelling the subtype relationship between UnliftedType and Type. The way data-elevator is unsafe (also) because GHC is free to move around coercions, which it wouldn’t if they were unidirectional.
Take a look at this:
https://hackage.haskell.org/package/coercible-subtypes-0.3.0.0/docs/Data-Type-Coercion-Sub.html
That’s a really cool library! And likely to help with the OP as well. But it doesn’t really help with my use case above because the coercion is heterogenous, i.e., it goes from one levity to another (nasty stuff).