Unidirectional Coercible

[int-index]

For newtypes that guarantee some invariant, we might want to coerce in one direction (unwrap) but not the other.

newtype NonNegative a = NonNegative a

coerce :: NonNegative a -> a -- safe
coerce :: a -> NonNegative a -- unsafe

Right now the only option is to not export the constructor, which makes both directions of coerce unavailable.

[nomeata]

This has been in the back of our heads for a while. But there are a few can of worms, such as now type constructors have not only roles, but also variances....

[goldfirere]

I agree that this would be nice, but doing it right would take at least one peer-reviewed publication, perhaps more. Indeed we would need variances, but we also need a new theory of FC/Core that can deal with non-symmetrical coercions. This would be interesting for me to pursue (and it's related to ideas I've wanted to write about), but no one should hold their breath.

[monoidal]

Linear types could use unidirectional coerce :: (a ->. b) ->. (a -> b).

[goldfirere]

Is this ticket achieving any goal right now? I move to close it. This won't be solved anytime soon, I don't think.

[int-index]

Is this ticket achieving any goal right now?

It's a feature request.

This won't be solved anytime soon, I don't think.

If this is ground for closing, so be it. I think it's good to have it open as a reminder that this is a desired feature, but I don't feel strongly.

[goldfirere]

I actually agree with @int-index here. I will leave open and label accordingly.

(The close/open below is purely an accidental button press -- there is absolutely no intention there.)

[Ericson2314]

The axioms proposed to be removed in #274 could be added back as one-way coercions. This is better than the situations both with and without #274 because it avoids the cost and semantic change of eta-expansion.

[Icelandjack]

With dependent types is there a way to somehow add a proof obligation? Taking the NonNegative example as an example, pretending Coercible has user instances:

instance Coercible (NonNegative a) a

but in the other direction.. I assume this won't make sense but it doesn't hurt to ask

instance pi (x :: a). (Num a, Ord a, x >= 0) => Coercible a (NonNegative a)

[Ericson2314]

I like this.

One small tweak:

instance pi (x :: a). (Num a, Ord a, (x >= 0) ~ True) => Coercible a (NonNegative a)