How to expose coercions only one way?

Learn
11

Yes, the recursive parameter to S is redundant in this case. Sub is general purpose—it supports any finite total ordering.

I’m also presuming a willingness to rely upon ImpredicativeTypes (which is fair in modern GHC) or to evade such issues with newtype wrappers.

I confess I didn’t read the latter portion of the OP that closely, but I had thought that e.g. (\x -> x) :: [PrimeNumber] -> [AnyNumber] would just work, and that less direct coercions could be constructed by manual composition:

weaken :: PrimeNumber -> AnyNumber
weaken = \p -> p

co :: PrimeNumber -> Identity AnyNumber
co = coerce . weaken

Sadly it seems I was wrong about the former, but sadness comes hand in hand with unsafe magic:

type Repr :: (k1 -> k2) -> Constraint
type Repr f = forall a b. Coercible a b => Coercible (f a) (f b)

fsub :: (Functor f, Repr f) => f PrimeNumber -> f AnyNumber
fsub fp = unsafeCoerce fp
1 Like