Optics.Coerce isn't zero-cost

[adamgundry]

The current implementations of the coerce{S,T,A,B} functions in Optics.Coerce sometimes require traversing data structures and hence are not guaranteed to be zero-cost, unlike coerce. For example we have

instance Functor f => Profunctor (Star f) where
  rmap    g (Star k) = Star (fmap g . k)
  ...
  rcoerce' = rmap coerce

At the very least we should make it clear in the Optics.Coerce docs that coercion may involve a runtime cost. But perhaps it is possible to do better. For example, can we use QuantifiedConstraints on Coercible to fake a limited version of higher-order roles?

[phadej]

I thought that we can have (forall x y. Coercible x y => Coercible (p i x a) (p i y a)) => Profunctor p for our profunctors, but

newtype Re p s t i a b = Re { unRe :: p i b a -> p i t s }

screws that idea.

i.e. we either have to be "Coercible1" in both parameters a and b, or in neither.

[adamgundry]

I had a play with this (branch 351-coercibleN-experiment) and got surprisingly far defining a superclass Coercible3 of Profunctor where

type Coercible1 f = (forall a b . Coercible a b => Coercible (f a) (f b)) :: Constraint
type Coercible2 f = (forall a a' b b' . (Coercible a a', Coercible b b') => Coercible (f a b) (f a' b')) :: Constraint
type Coercible3 f = (forall a a' b b' c c' . (Coercible a a', Coercible b b', Coercible c c') => Coercible (f a b c) (f a' b' c')) :: Constraint

but there are a few problems:

• Essentially every occurrence of Functor, Applicative etc. needs to be accompanied by a Coercible1 constraint, and similarly with Arrow and Coercible2. Morally these should be superclasses, but it is doubtful if that will ever happen, not least because they rule out instances that obey the laws only outside an abstraction boundary (https://ryanglscott.github.io/2018/06/22/quantifiedconstraints-and-the-trouble-with-traversable/). In particular this applies for converting between the profunctor and van Laarhoven representations.
• StarA and IxStarA are the only profunctors in Data.Profunctor.Indexed that fail to type-check. I haven't investigated why in detail, but I think the polymorphic component trips up the constraint solver. In principle those wouldn't be needed if we had a Pointed superclass of Applicative, but that also seems unlikely any time soon.
• The default implementations of ilinear and iwander no longer type-check, although inlining them into the instances succeeds. I guess this is incompleteness in the Coercible solver in the presence of QuantifiedConstraints, possibly https://gitlab.haskell.org/ghc/ghc/-/issues/15639?
• There are a few other cases where definitions don't type-check for unclear reasons, possibly similar.

I don't think this is a feasible approach now, but maybe in 10 years...

[phadej]

but it is doubtful if that will ever happen, not least because they rule out instances that obey the laws only outside an abstraction boundary

I think that the latter is a myth. See https://oleg.fi/gists/posts/2019-07-31-fmap-coerce-coerce.html#functor-should-be-parametric

[adamgundry]

@phadej interesting, thanks. I knew I had seen something discussing this before, but a quick search turned up only Ryan's post. Still, given how long AMP took, I can't imagine a QuantifiedConstraints superclass on Functor happening in short order...

[treeowl]

@phadej the only practical concern with wrapping a Coercible constraint in Mag is that said constraint won't be unpacked and every leaf of the structure will be one word larger than necessary. There is no way to represent unpacked Coercible evidence in a Haskell GADT, though Core is perfectly capable of doing so. This is very annoying.